Abstract
Given a timed automaton P modeling an implementation and a timed automaton S as a specification, the problem of
language inclusion checking is to decide whether the language of P is a subset of that of S. It is known to be undecidable. The problem
gets more complicated if non-Zenoness is taken into consideration. A run is Zeno if it permits infinitely many actions within finite time.
Otherwise it is non-Zeno. Zeno runs might present in both P and S. It is necessary to check whether a run is Zeno or not so as to avoid
presenting Zeno runs as counterexamples of language inclusion checking. In this work, we propose a zone-based semi-algorithm for
language inclusion checking with non-Zenoness. It is further improved with simulation reduction based on LU-simulation. Though our
approach is not guaranteed to terminate, we show that it does in many cases through empirical study. Our approach has been
incorporated into the PAT model checker, and applied to multiple systems to show its usefulness.
Original language | English |
---|---|
Pages (from-to) | - |
Journal | IEEE Transactions on Software Engineering |
DOIs | |
Publication status | Published - 16 Jan 2017 |