Is your Model Checker on Time? On the Complexity of Model Checking for Timed Modal Logics

Authors

  • Luca Aceto
  • Francois Laroussinie

DOI:

https://doi.org/10.7146/brics.v6i32.20101

Abstract

This paper studies the structural complexity of model checking
for (variations on) the specification formalisms used in the tools CMC
and Uppaal, and fragments of a timed alternation-free mu-calculus. For
each of the logics we study, we characterize the computational complexity
of model checking, as well as its specification and program complexity,
using timed automata as our system model.

Downloads

Published

1999-12-02

How to Cite

Aceto, L., & Laroussinie, F. (1999). Is your Model Checker on Time? On the Complexity of Model Checking for Timed Modal Logics. BRICS Report Series, 6(32). https://doi.org/10.7146/brics.v6i32.20101