Name
Title | ||
|---|---|---|
Verifying Temporal Properties of Sequential Machines Without Building their State Diagrams |
Abstract | ||
|---|---|---|
This paper presents the algorithm we have developed for proving that a finite state machine holds some properties expressed in temporal logic. This algorithm does not require the building of the state-transition graph nor the transition relation of the machine, so it overcomes the limits of the methods that have been proposed in the past. The verification algorithm presented here is based on Boolean function manipulations, which are represented by typed decision graphs. Thanks to this canonical representation, all the operations used in the algorithm have a polynomial complexity, expect for one called the computation of the critical term. The paper proposes techniques that reduce the computational cost of this operation. |
Year | DOI | Venue |
|---|---|---|
1990 | 10.1007/BFb0023716 | Computer Aided Verification |
Keywords | Field | DocType |
verifying temporal properties,state diagrams,sequential machines,canonical representation,temporal logic,boolean function,state diagram,finite state machine | Boolean function,Richards controller,State transition table,Interval temporal logic,Computer science,State diagram,Binary decision diagram,Extended finite-state machine,Algorithm,Finite-state machine,Theoretical computer science | Conference |
ISBN | Citations | PageRank |
3-540-54477-1 | 70 | 32.63 |
References | Authors | |
5 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Olivier Coudert | 1 | 665 | 104.87 |
| Jean Christophe Madre | 2 | 108 | 46.56 |
| Christian Berthet | 3 | 76 | 44.32 |