In: Lecture Notes in Computer Science, Vol. 1961: Advances in Computing Science, ASIAN 2000, pages 182-198. Springer-Verlag, 2000.
Abstract: This paper presents a framework for specifying and verifying an important class of hardware systems. These systems are built up from a parallel composition of circuit switching by a global clock. They can equivalently be characterized by Petri nets with a maximal step semantics. As a semantic model for these systems, distributed synchronous transition systems (DSTS) are proposed which are distributed transition systems with a global clock synchronizing the execution of actions. The relationship to asynchronous behavior of distributed transition systems is discussed employing Mazurkiewics trace theory which allows a uniform treatment of synchronous as well as asynchronous executions. A process algebra like calculus is introduced for defining DSTS which is called synchronous process systems. Furthermore, Foate linear time temporal logic (FLTL) is presented which is a temporal logic with a flavor of LTL adapted for specifying properties of DSTS. The contributions of this paper include the developed decision procedures for satisfiability as well as model checking of FLTL formulas, both based on alternating Buechi automata.
Keywords: Mazurkiewicz trace theory, Petri nets, alternating Buechi automata, distributed synchronous transition systems, linear temporal logics, model checking, process algebras, synchronized hardware circuits.