Computer Science Logic and 8th Kurt Gödel Colloquium
Detlef Kähler, Thomas Wilke: Program Complexity of Dynamic LTL Model Checking
Welcome and News
Host Institutions
Calls and Deadlines
Social Program
Location and Venue
Colocated Events
Authors' instructions
Print current pagePrint this page
Using a recent result by Hesse we show that for any fixed linear-time temporal formula the dynamic model checking problem is in Dyn-TC^0, a complexity class introduced by Hesse, Immerman, Patnaik, containing all dynamic problems where the update after an operation was performed can be computed by a DLOGTIME-uniform constant-depth threshold circuit. The operations permitted to modify the (transition) system to be verified include insertion and deletion of transitions and relabeling of states.
© 2002-2003 Kurt Gödel Society, Norbert Preining. 2003-06-04 Valid HTML 4.01! Valid CSS! Debian