Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

4-2014

Abstract

Given a timed automaton P modeling an implementation and a timed automaton S as a specification, language inclusion checking is to decide whether the language of P is a subset of that of S. It is known that this problem is undecidable and “this result is an obstacle in using timed automata as a specification language” [2]. This undecidability result, however, does not imply that all timed automata are bad for specification. In this work, we propose a zone-based semi-algorithm for language inclusion checking, which implements simulation reduction based on Anti-Chain and LU-simulation. Though it is not guaranteed to terminate, we show that it does in many cases through both theoretical and empirical analysis. The semi-algorithm has been incorporated into the PAT model checker, and applied to multiple systems to show its usefulness and scalability.

Keywords

Reachable State, Label Transition System, Boundedness Condition, Simulation Relation, Time Automaton

Discipline

Software Engineering | Theory and Algorithms

Research Areas

Software and Cyber-Physical Systems

Publication

Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Grenoble, France, April 5-13

First Page

310

Last Page

325

ISBN

9783030174651

Identifier

10.1007/978-3-642-54862-8_21

Publisher

Springer Link

City or Country

Grenoble, France

Additional URL

https://doi.org/10.1007/978-3-642-54862-8_21

Download

Share

COinS