Guarded Matching Logic is Decidable

Rodrigues, Nishant; Chen, Xiaohong; Rosu, Grigore

Permalink

https://hdl.handle.net/2142/112795 Copy

Description

Title

Guarded Matching Logic is Decidable

Author(s)

• Rodrigues, Nishant
• Chen, Xiaohong
• Rosu, Grigore

Issue Date

2021-11-30

Keyword(s)

• matching-logic
• decidablity

Abstract

Matching logic is the logical foundation of the K framework, where formal semantics of programming languages can be defined and language tools are automatically generated from the semantics. To bring more automation to K and its formal reasoning tools, we need to study decision procedures for matching logic. In this paper, we present three increasingly powerful decidable fragments of matching logic. The first, ``modal matching logic'', does not allow fixedpoints or quantification and is akin to multimodal polyadic modal logic. The second, ``quantifier-free matching logic'', extends this to allow fixedpoints. Finally, ``guarded matching logic'', allows both fixedpoints and quantification, albiet in a carefully restricted form. We prove that each of these fragments are decidabile, and several existing decidability results for modal mu-calculus, infinite- and finite-trace linear temporal logic, computation tree logic, and dynamic logic are all corollaries.

Type of Resource

text

Language

en

Permalink

http://hdl.handle.net/2142/112795

Owning Collections