Computer Science Logic and 8th Kurt Gödel Colloquium
Marko Samer, Helmut Veith: Validity of CTL Queries Revisited
Welcome and News
Host Institutions
Calls and Deadlines
Program
Social Program
Registration
Location and Venue
Accommodation
Committees
Contact
Colocated Events
Authors' instructions
Print current pagePrint this page
We systematically investigate temporal logic queries in model checking, adding to the seminal paper by William Chan at CAV 2000. Chan's temporal logic queries are CTL specifications where one unspecified subformula is to be filled in by the model checker in such a way that the specification becomes true. Chan defined a fragment of CTL queries called CTL-v which guarantees the existence of a unique strongest solution. The starting point of our paper is a counterexample to this claim. We then show how the research agenda of Chan can be realized by modifying his fragment appropriately. To this aim, we investigate the criteria required by Chan, and define two new fragments CTL-vNew and CTL-d where the first is the one originally intended; the latter fragment also provides unique strongest solutions where possible but admits also cases where the set of solutions is empty.
© 2002-2003 Kurt Gödel Society, Norbert Preining. 2003-06-04 Valid HTML 4.01! Valid CSS! Debian