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.