LORETO: a tool for reducing state explosion in verification of LOTOS programs

LOTOS is a formal specification language for concurrent and distributed sys tems. Basic LOTOS is the version of LOTOS without value-passing. A widely u sed approach to the verification of temporal properties is model checking. Often, in this approach the formal specification is translated into a label ed transition system on which formulae expressing properties are checked. A problem with this verification technique is state explosion: concurrent sy stems are often represented by automata with a prohibitive number of states . In this paper we show how, given a set rho of actions, it is possible to automatically obtain for a Basic LOTOS program a reduced transition system to which only the arcs labeled by actions in rho belong. The set rho of act ions plays a fundamental role in conjunction with a temporal logic defined by the authors in a previous paper: selective mu-calculus. The reduced syst em with respect to rho preserves the truth value of all selective mu-calcul us formulae with actions from the set rho. We act at both syntactic and sem antic levels. From a syntactic point of view, we define a set of transforma tion rules obtaining a smaller program. On the semantic side, we define a n on-standard semantics which dynamically reduces the transition system durin g generation, We present a tool implementing both the syntactic and the sem antic reduction. Copyright (C) 1999 John Wiley & Sons, Ltd.