Revisiting Timed Specification Theories: A Linear-Time Perspective
From MaRDI portal
Publication:4649387
DOI10.1007/978-3-642-33365-1_7zbMATH Open1374.68274arXiv1206.4504OpenAlexW1786563508MaRDI QIDQ4649387
M. Kwiatkowska, Chris Chilton, X. Wang
Publication date: 21 November 2012
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
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.
Full work available at URL: https://arxiv.org/abs/1206.4504
Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items (3)
An algebraic theory of interface automata ⋮ A Linear-Time–Branching-Time Spectrum of Behavioral Specification Theories ⋮ Progress-preserving Refinements of CTA
Uses Software
This page was built for publication: Revisiting Timed Specification Theories: A Linear-Time Perspective
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4649387)
