Soundness and Completeness of a Model-Checking Proof System for CTL

Autor:	Schuppe, Georg Friedrich, Gurov, Dilian
Rok vydání:	2023
Předmět:	Computer Science - Logic in Computer Science 68Q60 F.3.0
Druh dokumentu:	Working Paper
Popis:	We propose a local model-checking proof system for a fragment of CTL. The rules of the proof system are motivated by the well-known fixed-point characterisation of CTL based on unfolding of the temporal operators. To guarantee termination of proofs, we tag the sequents of our proof system with the set of states that have already been explored for the respective temporal formula. We define the semantics of tagged sequents, and then state and prove soundness and completeness of the proof system, as well as termination of proof search for finite-state models. Comment: 10 pages
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/2309.05389 Zobrazit plný text záznamu View this record from Arxiv