Model Checking Temporal Properties of Presburger Counter Systems

Abstract

Counter systems are a well-known and powerful modeling notation for specifying infnite state systems. In this thesis we target the problem of checking temporal properties of counter systems. We address three predominant families of temporal property specifications, namely Computation Tree Logics (CTL and CTL*) and Linear Temporal Logic (LTL). We provide two novel techniques to model check LTL and CTL properties of counter systems. We then provide a third technique to model check CTL temporal properties, which uses our LTL model checking technique as a sub-routine and is a modified version of an existing technique for finite-state systems. Each of our techniques returns a Presburger formula, which encodes the set of reachable states of the given system that satisfy the given temporal property. A novel aspect of our techniques is that they perform iterative analysis using reachability analysis sub-routines of counter systems. This brings two advantages to the table. The first is that these algorithms are able to compute precise answers on a much wider class of systems than previous approaches. Secondly, they compute results by iterative expansion or contraction, and hence permit an over-approximated or under- approximated solution to be obtained at any point even in cases where termination may not occur.For each of the three techniques we propose in this thesis, we formally prove its correctness, and also give a theoretical characterization of the class of counter systems for which it can terminate with precise results. We also provide an implementation of our CTL and LTL model checking techniques. We present experimental results on standard benchmarks (such as cache coherence protocols, communication protocols, control mechanisms etc. modeled as counter systems), which demonstrate the precision as well as efficiency of our techniques.