Symbolic techniques for parametric reasoning about counter and clock systems. (English) Zbl 0974.68523

Annichini, Aurore; Asarin, Eugene; Bouajjani, Ahmed

Emerson, E. Allen (ed.) et al., Computer aided verification. 12th international conference, CAV 2000. Chicago, IL, USA, July 15-19, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1855, 419-434 (2000).

Summary: We address the problem of automatic analysis of parametric counter and clock automata. We propose a semi-algorithmic approach based on using (1) expressive symbolic representation structures called Parametric DBM’s, and (2) accurate extrapolation techniques allowing to speed up the reachability analysis and help its termination. The techniques we propose consist in guessing automatically the effect of iterating a control loop an arbitrary number of times, and in checking that this guess is exact. Our approach can deal uniformly with systems that generate linear or nonlinear sets of configurations. We have implemented our techniques and experimented them on nontrivial examples such as a parametric timed version of the bounded retransmission protocol.
For the entire collection see [Zbl 0941.00029].

MSC:

68Q60	Specification and verification (program logics, model checking, etc.)
68Q45	Formal languages and automata

Software:

REDLOG