Since usually no scheduler is given at the programming or modeling language level, abstract models together with a refinement notion are necessary to model concurrent systems adequately. Deterministic transition systems are an appropriate model for implementations of (concurrent) reactive programs based on synchronous communication. In this paper, we develop a suitable setting for modeling and reasoning about deterministic transition systems. In particular, we (i) develop a class of abstract models together with a refinement notion; (ii) define parallel composition guaranteeing fairness; and (iii) develop a 3-valued logic with a satisfaction relation that is preserved under refinement. © Springer-Verlag Berlin Heidelberg 2007.
CITATION STYLE
Fecher, H., & Grabe, I. (2007). Finite abstract models for deterministic transition systems: Fair parallel composition and refinement-preserving Logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4767 LNCS, pp. 1–16). Springer Verlag. https://doi.org/10.1007/978-3-540-75698-9_1
Mendeley helps you to discover research relevant for your work.