Detecting Quasi-equal Clocks in Timed Automata
- 499 Downloads
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.
Unable to display preview. Download preview PDF.
- 4.Bellman, R., Kalaba, R.E.: Dynamic programming and modern control theory. Academic Press, New York (1965)Google Scholar
- 7.Daws, C., Yovine, S.: Reducing the number of clock variables of timed automata. In: Proc. RTSS 1996, pp. 73–81. IEEE Computer Society Press (1996)Google Scholar
- 14.Olderog, E.R., Dierks, H.: Real-Time Systems - Formal Specification and Automatic Verification. Cambridge University Press (2008)Google Scholar
- 15.Pettersson, P.: Modelling and verification of real-time systems using timed automata: theory and practice. Ph.D. thesis, Citeseer (1999)Google Scholar
- 19.Zee, K., Kuncak, V., Rinard, M.: Full functional verification of linked data structures. In: Proceedings of the 2008 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2008, pp. 349–361. ACM, New York (2008), http://doi.acm.org/10.1145/1375581.1375624 CrossRefGoogle Scholar