Publication Type

Journal Article

Version

acceptedVersion

Publication Date

11-2017

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.

Keywords

Timed automata, language inclusion, non-Zenoness

Discipline

Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

IEEE Transactions on Software Engineering

Volume

43

Issue

11

First Page

995

Last Page

1008

ISSN

0098-5589

Identifier

10.1109/TSE.2017.2653778

Publisher

Institute of Electrical and Electronics Engineers (IEEE)

Copyright Owner and License

Authors

Additional URL

https://doi.org/10.1109/TSE.2017.2653778

Download

Share

COinS