Sound Conflict Analysis for Timed Contract Automata

TL;DR

This paper introduces a sound algorithm for conflict analysis in timed contract automata, extending discrete time deontic logic techniques to continuous time with a case study demonstration.

Contribution

It presents the first sound algorithm for conflict detection in timed contract automata, bridging a gap in real-time deontic logic analysis.

Findings

Algorithm is sound and correct

Effective conflict detection demonstrated on a case study

Extends discrete time methods to continuous time

Abstract

One can find various temporal deontic logics in literature, most focusing on discrete time. The literature on real-time constraints and deontic norms is much sparser. Thus, many analysis techniques which have been developed for deontic logics have not been considered for continuous time. In this paper we focus on the notion of conflict analysis which has been extensively studied for discrete time deontic logics. We present a sound, but not complete algorithm for detecting conflicts in timed contract automata and prove the correctness of the algorithm, illustrating the analysis on a case study.