Philosophy:Counterexample-guided abstraction refinement

From HandWiki
Short description: A technique for symbolic model checking and logic calculi

Counterexample-guided abstraction refinement (CEGAR) is a technique for symbolic model checking.[1][2] It is also applied in modal logic tableau calculi algorithms to optimise their efficiency.[3]

In computer-aided verification and analysis of programs, models of computation often consist of states. Models for even small programs, however, may have an enormous number of states. This is identified as the state explosion problem.[4] CEGAR addresses this problem with two stages — abstraction, which simplifies a model by grouping states, and refinement, which increases the precision of the abstraction to better approximate the original model.

If a desired property for a program is not satisfied in the abstract model, a counterexample is generated. The CEGAR process then checks whether the counterexample is spurious, i.e., if the counterexample also applies to the under-abstraction but not the actual program. If this is the case, it concludes that the counterexample is attributed to inadequate precision of the abstraction. Otherwise, the process finds a bug in the program. Refinement is performed when a counterexample is found to be spurious.[5] The iterative procedure terminates either if a bug is found or when the abstraction has been refined to the extent that it is equivalent to the original model.

Program verification

Abstraction

To reason about the correctness of a program, particularly those involving the concept of time for concurrency, state transition models are used. In particular, finite-state models can be used along with temporal logic in automatic verification.[6] The concept of abstraction is thus founded upon a mapping between two Kripke structures. Specifically, programs can be described with control flow automata (CFA).[7]

Define a Kripke structure [math]\displaystyle{ M }[/math] as [math]\displaystyle{ \langle S, s_0, R, L\rangle }[/math], where

  • [math]\displaystyle{ S }[/math] is a finite set of states,
  • [math]\displaystyle{ s_0 }[/math] is an initial state in [math]\displaystyle{ S }[/math],
  • [math]\displaystyle{ R }[/math] is a total transition relation, and
  • [math]\displaystyle{ L }[/math] is a function that labels each state with a set of propositional names that hold therein.

An abstraction of [math]\displaystyle{ M }[/math] is defined by [math]\displaystyle{ \langle S_\alpha, s_0^\alpha, R_\alpha, L_\alpha \rangle }[/math] where [math]\displaystyle{ \alpha }[/math] is an abstraction mapping that maps every state in [math]\displaystyle{ S }[/math] to a state in [math]\displaystyle{ S_\alpha }[/math].[5]

To preserve the critical properties of the model, the abstraction mapping maps the initial state in the original model [math]\displaystyle{ s_0 }[/math] to its counterpart [math]\displaystyle{ s_0^\alpha }[/math] in the abstract model. The abstraction mapping also guarantees that the transition relations between two states are preserved.

Model Checking

In each iteration, model checking is performed for the abstract model. Bounded model checking, for instance, generates a propositional formula that is then checked for Boolean satisfiability by a SAT solver.[5]

Refinement

When counterexamples are found, they are examined to determine if they are spurious examples, i.e., they are unauthentic ones that emerge from the under-abstraction of the model. A non-spurious counterexample reflects the incorrectness of the program, which may be sufficient to terminate the program verification process and conclude that the program is incorrect. The main objective of the refinement process handle spurious counterexamples. It eliminates them by increasing the granularity of the abstraction.

The refinement process ensures that the dead-end states and the bad states do not belong to the same abstract state. A dead-end state is a reachable one with no outgoing transition whereas a bad-state is one with transitions causing the counterexample. [2]

Tableau calculi

Since modal logic is often interpreted with Kripke semantics, where a Kripke frame resembles the structure of state transition systems concerned in program verification, the CEGAR technique is also implemented for automated theorem proving.[3]

References

  1. ↑ Clarke, Edmund; Grumberg, Orna; Jha, Shomesh; Lu, Yuan; Veith, Helmut (1 September 2003). "Counterexample-guided abstraction refinement for symbolic model checking". Journal of the ACM 50 (5): 752-794. doi:10.1145/876638.876643. https://dl.acm.org/doi/10.1145/876638.876643. 
  2. ↑ 2.0 2.1 Clarke, Edmund; Grumberg, Orna; Jha, Shomesh; Lu, Yuan; Veith, Helmut (2000). "Counterexample-Guided Abstraction Refinement". International Conference on Computer Aided Verification CAV 2000: Computer Aided Verification. 1855. Berlin, Heidelberg: Springer. pp. 154-169. doi:10.1007/10722167_15. ISBN 978-3-540-45047-4. https://link.springer.com/chapter/10.1007/10722167_15. 
  3. ↑ 3.0 3.1 Goré, Rajeev; Kikkert, Cormac (6 September 2021). "CEGAR-Tableaux: Improved Modal Satisfiability via Modal Clause-Learning and SAT". Automated Reasoning with Analytic Tableaux and Related Methods: 30th International Conference, TABLEAUX 2021, Birmingham, UK. 12842. Cham: Springer. pp. 74-91. doi:10.1007/978-3-030-86059-2_5. ISBN 978-3-030-86059-2. https://link.springer.com/chapter/10.1007/978-3-030-86059-2_5. 
  4. ↑ Valmari, Antti (1998). "The State Explosion Problem". Advanced Course on Petri Nets, ACPN 1996. 1491. Berlin, Heidelberg: Springer. pp. 429–528. doi:10.1007/978-3-642-35746-6_1. ISBN 978-3-540-49442-3. https://link.springer.com/chapter/10.1007/3-540-65306-6_21. Retrieved 27 December 2023. 
  5. ↑ 5.0 5.1 5.2 Clarke, Edmund; Klieber, William; Nováček, Miloš; Zuliani, Paolo (2011). "Model Checking and the State Explosion Problem". LASER Summer School on Software Engineering: LASER 2011. 7682. p. 1–30. doi:10.1007/978-3-642-35746-6_1. ISBN 978-3-642-35746-6. https://link.springer.com/chapter/10.1007/978-3-642-35746-6_1. Retrieved 27 December 2023. 
  6. ↑ Clarke, Edmund; Browne, Michael C.; Emerson, E. Allen; Sistla, A.P.. "Using Temporal Logic for Automatic Verification of Finite State Systems". 13. Berlin, Heidelberg: Springer. doi:10.1007/978-3-642-82453-1_1. ISBN 978-3-642-82453-1. https://link.springer.com/chapter/10.1007/978-3-642-82453-1_1. 
  7. ↑ Hajdu, Ákos; Micskei, Zoltán (11 November 2019). "Efficient Strategies for CEGAR-Based Model Checking". Journal of Automated Reasoning (Springer Nature) 64 (4): 1051–1091. doi:10.1007/s10817-019-09535-x. 



Retrieved from "https://handwiki.org/wiki/index.php?title=Philosophy:Counterexample-guided_abstraction_refinement&oldid=3286866"