Are timed automata bad for a specification language? Language inclusion checking for timed automata

• Main Authors: WANG, Ting, SUN, Jun, LIU, Yang, WANG, Xinyu, LI, Shanping
• Format: text
• Language: English
• Published: Institutional Knowledge at Singapore Management University 2014
• Subjects: Reachable State; Label Transition System; Boundedness Condition; Simulation Relation; Time Automaton; Software Engineering; Theory and Algorithms
• Online Access: https://ink.library.smu.edu.sg/sis_research/4957; https://ink.library.smu.edu.sg/context/sis_research/article/5960/viewcontent/Wang2014_Chapter_AreTimedAutomataBadForASpecifi.pdf
• Institution: Singapore Management University

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.