Veronique Bruyere ; Jean-Francois Raskin - Real-Time Model-Checking: Parameters everywhere

lmcs:2229 - Logical Methods in Computer Science, February 27, 2007, Volume 3, Issue 1 - https://doi.org/10.2168/LMCS-3(1:7)2007
Real-Time Model-Checking: Parameters everywhereArticle

Authors: Veronique Bruyere ; Jean-Francois Raskin

    In this paper, we study the model-checking and parameter synthesis problems of the logic TCTL over discrete-timed automata where parameters are allowed both in the model (timed automaton) and in the property (temporal formula). Our results are as follows. On the negative side, we show that the model-checking problem of TCTL extended with parameters is undecidable over discrete-timed automata with only one parametric clock. The undecidability result needs equality in the logic. On the positive side, we show that the model-checking and the parameter synthesis problems become decidable for a fragment of the logic where equality is not allowed. Our method is based on automata theoretic principles and an extension of our method to express durations of runs in timed automata using Presburger arithmetic.


    Volume: Volume 3, Issue 1
    Published on: February 27, 2007
    Submitted on: July 19, 2005
    Keywords: Computer Science - Logic in Computer Science,F.1.1

    21 Documents citing this article

    Consultation statistics

    This page has been seen 1424 times.
    This article's PDF has been downloaded 472 times.