TY - GEN

T1 - A formalisation of consistent consequence for boolean equation systems

AU - van Delft, M.

AU - Geuvers, H.

AU - Willemse, T.A.C.

PY - 2017

Y1 - 2017

N2 - Boolean equation systems are sequences of least and greatest fixpoint equations interpreted over the Boolean lattice. Such equation systems arise naturally in verification problems such as the modal α-calculus model checking problem. Solving a Boolean equation system is a computationally challenging problem, and for this reason, abstraction techniques for Boolean equation systems have been developed. The notion of consistent consequence on Boolean equation systems was introduced to more effectively reason about such abstraction techniques. Prior work on consistent consequence claimed that this notion can be fully characterised by a sound and complete derivation system, building on rules for logical consequence. Our formalisation of the theory of consistent consequence and the derivation system in the proof assistant Coq reveals that the system is, nonetheless, unsound. We propose a fix for the derivation system and show that the resulting system (system CC) is indeed sound and complete for consistent consequence. Our formalisation of the consistent consequence theory furthermore points at a subtle mistake in the phrasing of its main theorem, and how to correct this.

AB - Boolean equation systems are sequences of least and greatest fixpoint equations interpreted over the Boolean lattice. Such equation systems arise naturally in verification problems such as the modal α-calculus model checking problem. Solving a Boolean equation system is a computationally challenging problem, and for this reason, abstraction techniques for Boolean equation systems have been developed. The notion of consistent consequence on Boolean equation systems was introduced to more effectively reason about such abstraction techniques. Prior work on consistent consequence claimed that this notion can be fully characterised by a sound and complete derivation system, building on rules for logical consequence. Our formalisation of the theory of consistent consequence and the derivation system in the proof assistant Coq reveals that the system is, nonetheless, unsound. We propose a fix for the derivation system and show that the resulting system (system CC) is indeed sound and complete for consistent consequence. Our formalisation of the consistent consequence theory furthermore points at a subtle mistake in the phrasing of its main theorem, and how to correct this.

UR - http://www.scopus.com/inward/record.url?scp=85029528300&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-66107-0_29

DO - 10.1007/978-3-319-66107-0_29

M3 - Conference contribution

AN - SCOPUS:85029528300

SN - 9783319661063

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 462

EP - 478

BT - Interactive theorem proving - 8th International Conference, ITP 2017,Proceedings

A2 - Ayala-Rincón, Mauricio

A2 - Muñoz, César A.

PB - Springer

T2 - 8th International Conference on Interactive Theorem Proving, ITP 2017

Y2 - 26 September 2017 through 29 September 2017

ER -