LTL Model Checking in Matching Logic

Tusil, Jan; Chen, Xiaohong

Permalink

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

Description

Title

LTL Model Checking in Matching Logic

Author(s)

• Tusil, Jan
• Chen, Xiaohong

Issue Date

2022-05

Keyword(s)

• LTL
• model checking
• matching logic

Abstract

Matching logic is a logic that serves as the foundation of the K formal semantics framework. Through K, many programming languages have been given formal semantics in the form of a matching logic theory. The K framework is then a best-effort implementation of matching logic reasoning. In this paper, we investigate the problem of LTL model checking of (potentially infinite) systems specified as matching logic theories. In particular, we construct a theory Gamma^MC such that for any matching logic theory Gamma^S (respecting certain syntactical constraints) representing a Kripke structure S and for any LTL formula phi, the structure S satisfies phi iff phi is valid in the joint theory Gamma^S U Gamma^MC. This way, one can reason about the model checking problem using matching logic's sound proof system. With this work, we hope to lay out the theoretical foundations for implementing LTL model checking in the K framework, as well as to establish a connection between model checking and theorem proving.

Type of Resource

text

Language

en

Permalink

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

Owning Collections