Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Sound Conflict Analysis for Timed Contract Automata

Shaun Azzopardi, Gordon Pace

TL;DR

A sound, but not complete algorithm for detecting conflicts in timed contract automata is presented and the correctness of the algorithm is proved, illustrating the analysis on a case study.

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.

Sound Conflict Analysis for Timed Contract Automata

TL;DR

A sound, but not complete algorithm for detecting conflicts in timed contract automata is presented and the correctness of the algorithm is proved, illustrating the analysis on a case study.

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.

Paper Structure

This paper contains 11 sections, 15 theorems, 4 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Background
  3. Normative Conflicts
  4. From Persistent Norms to Ephemeral Norms
  5. Abstracting active norms:
  6. Timing conditions:
  7. Translation:
  8. Conflict Analysis
  9. Case Study
  10. Conclusions
  11. Proofs

Key Result

Lemma 1

For all time points $v$ and non-empty actions $p:a$, $active(N, (p:a, v)) \in \textit{active}_\alpha(N, p:a)$.

Figures (1)

  • Figure 1: Part of automaton corresponding to the case study constraints.

Theorems & Definitions (23)

  • Definition 1
  • Definition 2
  • Lemma 1
  • Lemma 2
  • Lemma 3
  • Lemma 4
  • Lemma 5
  • proof
  • Lemma 6
  • Theorem 1
  • ...and 13 more