TY - JOUR AU - Aceto, Luca AU - Laroussinie, Francois PY - 1999/12/02 Y2 - 2024/03/29 TI - Is your Model Checker on Time? On the Complexity of Model Checking for Timed Modal Logics JF - BRICS Report Series JA - BRICS VL - 6 IS - 32 SE - Articles DO - 10.7146/brics.v6i32.20101 UR - https://tidsskrift.dk/brics/article/view/20101 SP - AB - This paper studies the structural complexity of model checking<br />for (variations on) the specification formalisms used in the tools CMC<br />and Uppaal, and fragments of a timed alternation-free mu-calculus. For<br />each of the logics we study, we characterize the computational complexity<br />of model checking, as well as its specification and program complexity,<br />using timed automata as our system model. ER -