Verification and comparison of transition systems

Abstract

The notion of a transition system is of fundamental importance for studying the semantics of systems of interacting processes. Firstly, this notion is convenient for modeling these systems. In particular, the synchronized product of transition systems allows us to describe a system from the description, by transition systems, of its components, and from a description of the interactions between these components by giving the actions or events that may simultaneously occur in the system. Secondly, the notion of a transition system is the basis on which one can develop semantic notions such as verification of properties, by designing logics having transition systems as models, or comparison of transition systems, by structural equivalences defined by homomorphisms or logical equivalences related to logics [or transition systems. In this paper we present a short survey of these basic notions.