Program Complexity of Dynamic LTL Model Checking

Abstract 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 has been 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.

Authors

• Detlef Kähler
• Thomas Wilke

Keywords

No keywords are indexed for this paper.