TY - GEN
T1 - Detecting quasi-equal clocks in timed automata
AU - Muñiz, Marco
AU - Westphal, Bernd
AU - Podelski, Andreas
PY - 2013/8/28
Y1 - 2013/8/28
N2 - A recent optimizations technique for timed model checking starts with a given specification of quasi-equal clocks. In principle, the zone graph can used to detect which clocks are quasi-equal; the construction of the zone graph would, however, defeat its very purpose (which is the optimization of this construction). In this paper, we present an abstraction that is effective for the goal of the optimization based on quasi-equal clocks: it is coarse enough to yield a drastic reduction of the size of the zone graph. Still, it is precise enough to identify a large class of quasi-equal clocks. The abstraction is motivated by an intuition about the way quasi-equalities can be tracked. We have implemented the corresponding reasoning method in the Jahob framework using an SMT solver. Our experiments indicate that our intuition may lead to a useful abstraction.
AB - A recent optimizations technique for timed model checking starts with a given specification of quasi-equal clocks. In principle, the zone graph can used to detect which clocks are quasi-equal; the construction of the zone graph would, however, defeat its very purpose (which is the optimization of this construction). In this paper, we present an abstraction that is effective for the goal of the optimization based on quasi-equal clocks: it is coarse enough to yield a drastic reduction of the size of the zone graph. Still, it is precise enough to identify a large class of quasi-equal clocks. The abstraction is motivated by an intuition about the way quasi-equalities can be tracked. We have implemented the corresponding reasoning method in the Jahob framework using an SMT solver. Our experiments indicate that our intuition may lead to a useful abstraction.
UR - http://www.scopus.com/inward/record.url?scp=84882780084&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-40229-6_14
DO - 10.1007/978-3-642-40229-6_14
M3 - Article in proceeding
AN - SCOPUS:84882780084
SN - 9783642402289
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 198
EP - 212
BT - Formal Modeling and Analysis of Timed Systems - 11th International Conference, FORMATS 2013, Proceedings
T2 - 11th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2013
Y2 - 29 August 2013 through 31 August 2013
ER -