Abstract | ||
---|---|---|
We present a tableau system for the model checking problem of the linear time /*-calculus. It improves the system of Stifling and Walker by simplifying the success condition for a tableau. In our system success for a leaf is determined by the path leading to it, whereas Stifling and Walker's method requires the examination of a potentially infinite number of paths extending over the whole tableau. |
Year | DOI | Venue |
---|---|---|
1996 | 10.1007/3-540-61440-0_120 | ICALP |
Keywords | Field | DocType |
temporal logic,linear time,linear-time #-calculus,tableau systems,local model-checking,effective tableau system,model checking | Discrete mathematics,Combinatorics,Model checking,Temporal logic,Time complexity,Mathematics,Calculus,Stirling engine | Conference |
ISBN | Citations | PageRank |
3-540-61440-0 | 4 | 0.80 |
References | Authors | |
7 | 3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Julian C. Bradfield | 1 | 319 | 29.46 |
Javier Esparza | 2 | 513 | 39.11 |
Angelika Mader | 3 | 199 | 19.44 |