We introduce Symbolic Timed Automata, an amalgamation of symbolic transition systems and timed automata, which allows to express nondeterministic data-dependent control flow with inputs and outputs and real-time behaviour. In particular, input data can influence the timing behaviour. We define two semantics for STA, a concrete one as timed labelled transition systems and another one on a symbolic level. We show that the symbolic semantics is complete and correct w.r.t. the concrete one. Finally, we introduce symbolic conformance relation stioco , which is an extension of the well-known ioco conformance relation. Relation stioco is defined using FO-logic on a purely symbolic level. We show that stioco corresponds on the concrete semantic level to Krichen and Tripakis’ implementation relation tioco for timed labelled transition systems.
|Title of host publication||Formal Modeling and Analysis of Timed Systems (8th International Conference, FORMATS 2010, Klosterneuburg, Austria, September 8-10, 2010. Proceedings)|
|Editors||K. Chatterjee, T.A. Henzinger|
|Place of Publication||Berlin|
|Publication status||Published - 2010|
|Name||Lecture Notes in Computer Science|