Name
Abstract | ||
|---|---|---|
This paper examines FLC, which is the modal 碌-calculus enriched with a sequential composition operator. Bisimulation invariance and the tree model property are proved. Its succinctness is compared to the modal 碌-calculus. The main focus lies on FLC's model checking problem over finite transition systems. It is proved to be PSPACE-hard. A tableau model checker is given and an upper EXPTIME bound is derived from it. For a fixed alternation depth FLC's model checking problem turns out to be PSPACE-complete. |
Year | DOI | Venue |
|---|---|---|
2002 | 10.1007/3-540-45931-6_18 | FoSSaCS |
Keywords | Field | DocType |
main focus,bisimulation invariance,tree model property,tableau model checker,fixed alternation depth,upper exptime,sequential composition operator,model checking problem,model checking fixed point,finite transition system,model checking,fixed point,composition operator | Transition system,Discrete mathematics,Model checking,EXPTIME,Succinctness,Algorithm,Modal logic,Bisimulation,Temporal logic,Fixed point,Mathematics | Conference |
Volume | ISSN | ISBN |
2303 | 0302-9743 | 3-540-43366-X |
Citations | PageRank | References |
392 | 13.54 | 7 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Martin Lange | 1 | 447 | 22.83 |
| Colin Stirling | 2 | 934 | 102.50 |