Continuous action system refinement

Larissa Meinicke*, Ian J. Hayes

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contributionpeer-review

7 Citations (Scopus)

Abstract

Action systems are a framework for reasoning about discrete reactive systems. Back, Petre and Porres have extended these action systems to continuous action systems, which can be used to model hybrid systems. In this paper we define a refinement relation, and develop practical data refinement rules for continuous action systems. The meaning of continuous action systems is expressed in terms of a mapping from continuous action systems to action systems. First, we present a new mapping from continuous action systems to action systems, such that Back's definition of trace refinement is correct with respect to it. Second, we present a stream semantics that is compatible with the trace semantics, but is preferable to it because it is more general. Although action system trace refinement rules are applicable to continuous action systems with a stream semantics, they are not complete. Finally, we introduce a new data refinement rule that is valid with respect to the stream semantics and can be used to prove refinements that are not possible in the trace semantics, and we analyse the completeness of our new rule in conjunction with the existing trace refinement rules.

Original languageEnglish
Title of host publicationMathematics of Program Construction - 8th International Conference, MPC 2006, Proceedings
EditorsTarmo Uustalu
PublisherSpringer, Springer Nature
Pages316-337
Number of pages22
Volume4014 LNCS
ISBN (Print)3540356312, 9783540356318
DOIs
Publication statusPublished - 2006
Event8th International Conference on Mathematics of Program Construction, MPC 2006 - Kuressaare, Estonia
Duration: 3 Jul 20065 Jul 2006

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4014 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other8th International Conference on Mathematics of Program Construction, MPC 2006
CountryEstonia
CityKuressaare
Period3/07/065/07/06

Fingerprint Dive into the research topics of 'Continuous action system refinement'. Together they form a unique fingerprint.

Cite this