Abstract
We extend CTL logic to a logic called COUNT CTL (CCTL) for specifying properties of concurrent programs with large number of processes. We present a model checking algorithm for symmetric or partially symmetric systems when their correctness specification is given in CCTL. The model-checking algorithm employs Guarded Quotient Structures introduced in [9]. The GQS structures can be succinct representations for the reachability graphs of partially symmetric or even asymmetric systems. Our algorithm exploits state symmetries for fast evaluation. The algorithm is top down in nature, and automatically incorporates formula decomposition and sub-formula tracking.
Keywords
Correctness
Model checking
Quotient
Computer science
Reachability
CTL*
Algorithm
Theoretical computer science
Computation tree logic
State (computer science)
Mathematics
Combinatorics
Subject Areas
Formal Methods in Verification
·Computational Theory and Mathematics ·Physical Sciences
Logic, programming, and type systems
·Artificial Intelligence ·Physical Sciences
semigroups and automata theory
·Computational Theory and Mathematics ·Physical Sciences
Loading…