Abstract
Modal transition systems specify sets of implementations, their refining labelled transition systems, through Larsen & Thomsen’s co-inductive notion of refinement. We demonstrate that refinement precisely captures the identification of a modal transition system with its set of implementations: refinement is reverse containment of sets of implementations. This result extends to models that combine state and event observables and is drawn from a SFP-domain whose elements are equivalence classes of modal transition systems under refinement [HJS04], and abstraction-based finite-model properties proved in this paper. As a corollary, validity checking is model checking for Hennessy-Milner formulas that characterize modal transition systems with bounded computation paths. We finally sketch how techniques developed in this paper can be used to detect inconsistencies between multiple modal transition systems and, if consistent, to verify properties of all common implementations.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
Author information
Authors and Affiliations
Corresponding author
Additional information
Received January 2004
Revised August 2004
Accepted December 2004 by M. Leuschel and D. J. Cooke
Rights and permissions
About this article
Cite this article
Huth, M. Refinement is complete for implementations. Form Asp Comp 17, 113–137 (2005). https://doi.org/10.1007/s00165-005-0063-z
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-005-0063-z