Revisiting Timed Specification Theories: A Linear-Time Perspective

TL;DR

This paper introduces a new compositional specification theory for timed automata that supports component substitution, parallel composition, and synthesis, ensuring safety and liveness properties are preserved in real-time systems.

Contribution

It presents a novel timed specification theory based on linear-time semantics, enabling compositional reasoning and incremental synthesis for real-time systems with critical timing constraints.

Findings

Defines a weakest congruence preserving safety and bounded liveness

Characterizes the congruence using timed-traces and timed-strategies

Provides operations for component composition and synthesis in timed automata

Abstract

We consider the setting of component-based design for real-time systems with critical timing constraints. Based on our earlier work, we propose a compositional specification theory for timed automata with I/O distinction, which supports substitutive refinement. Our theory provides the operations of parallel composition for composing components at run-time, logical conjunction/disjunction for independent development, and quotient for incremental synthesis. The key novelty of our timed theory lies in a weakest congruence preserving safety as well as bounded liveness properties. We show that the congruence can be characterised by two linear-time semantics, timed-traces and timed-strategies, the latter of which is derived from a game-based interpretation of timed interaction.