Deriving Parameter Conditions for Periodic Timed Automata
Satisfying Real-Time Temporal Logic Formulas
Akio Nakata, Teruo Higashino
Department of Informatics and Mathematical Science, Osaka University
{nakata,higashino}@ics.es.osaka-u.ac.jp
Abstract
A symbolic model checking method for parametric periodic timed automata
is proposed.
The method derives symbolically the weakest condition
for parameters such that the specified control state of
a periodic timed automaton satisfies some temporal properties.
Unlike several existing parametric symbolic model checking methods,
the proposed method is `on-the-fly' ---
it does not unnecessarily check all the states.
Instead, it traverses some necessary part of the computation tree
to derive the weakest condition.
We show that if we constrain a timed automaton to be {\em periodic},
i.e. if we force a timed automaton to return to its initial state
periodically at the specified constant time,
we have only to traverse at most the first 3 periods
in the infinite computation tree.
In the proposed method, we can
avoid a costly (and generally undecidable) fixpoint-calculation
for dense-time-domain state sets,
and derive the weakest condition for parameters
of a timed automaton to satisfy given temporal properties
written in a real-time temporal logic formula.