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 Program Social Program Registration Location and Venue Accommodation Committees Contact Colocated Events Authors' instructions

Print 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