Real-Time Model-Checking: Parameters everywhere

TL;DR

This paper investigates the decidability of model-checking and parameter synthesis for TCTL over discrete-timed automata with parameters, showing undecidability with equality but decidability without it.

Contribution

It establishes undecidability results for TCTL with equality and decidability for a fragment without equality, extending automata-theoretic methods with Presburger arithmetic.

Findings

Model-checking with parameters is undecidable with equality.

Model-checking without equality is decidable for a fragment.

Automata-theoretic methods are extended using Presburger arithmetic.

Abstract

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.