LORETO: a tool for reducing state explosion in verification of LOTOS programs
✍ Scribed by Roberto Barbuti; Nicoletta De Francesco; Antonella Santone; Gigliola Vaglini
- Publisher
- John Wiley and Sons
- Year
- 1999
- Tongue
- English
- Weight
- 171 KB
- Volume
- 29
- Category
- Article
- ISSN
- 0038-0644
No coin nor oath required. For personal study only.
✦ Synopsis
LOTOS is a formal specification language for concurrent and distributed systems. Basic LOTOS is the version of LOTOS without value-passing. A widely used approach to the verification of temporal properties is model checking. Often, in this approach the formal specification is translated into a labeled transition system on which formulae expressing properties are checked. A problem with this verification technique is state explosion: concurrent systems are often represented by automata with a prohibitive number of states. In this paper we show how, given a set ρ 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 ρ belong. The set ρ of actions plays a fundamental role in conjunction with a temporal logic defined by the authors in a previous paper: selective mu-calculus. The reduced system with respect to ρ preserves the truth value of all selective mu-calculus formulae with actions from the set ρ. We act at both syntactic and semantic levels. From a syntactic point of view, we define a set of transformation rules obtaining a smaller program. On the semantic side, we define a non-standard semantics which dynamically reduces the transition system during generation. We present a tool implementing both the syntactic and the semantic reduction.