|
|
|
                                          
|
Return to Short Papers
Schnoebelen (2001) examined the decidability problem for liveness (reachability) and progress (eventuality) properties in well-structured single action transition systems. Our main result is as follows: the model checking problem is decidable for disjunctive formulae of the propositional µ-Calculus of D. Kozen (1983) in well-structured transition systems where propositional variables are interpreted by upward cones. We also discuss the model checking problem for the intuitionistic modal logic of Fisher Servi (1984) extended by least fixpoint.
@inproceedings{DBLP:conf/time/KouzminSS04, author = {E. V. Kouzmin and Nikolay V. Shilov and Valery A. Sokolov}, title = {Model Checking mu-Calculus in Well-Structured Transition Systems.}, booktitle = {TIME}, year = {2004}, pages = {152-155}, ee = {http://csdl.computer.org/comp/proceedings/time/2004/2155/00/21550152abs.htm}, crossref = {conf/time/2004}, bibsource = {DBLP, http://dblp.uni-trier.de} } @proceedings{DBLP:conf/time/2004, title = {11th International Symposium on Temporal Representation and Reasoning (TIME 2004), 1-3 July 2004, Tatihou Island, Normandie, France}, booktitle = {TIME}, publisher = {IEEE Computer Society}, year = {2004}, isbn = {0-7695-2155-X}, bibsource = {DBLP, http://dblp.uni-trier.de} } },  ©2005 Association for Computing Machinery |
