On the Complexity of Model Checking for Temporal Equilibrium Logic

Abstract

Bei einer LTL-Formel φ und einer Spur T besteht das Problem des Model Checkings für Temporal Equilibrium Logic (TEL) darin, zu bestimmen, ob T ein Temporal Equilibrium Model (TEM) von φ ist. Das Problem des Model Checkings, das bereits für mehrere andere prominente klassische Logiken, wie Linear Temporal Logic (LTL) und Computation Tree Logic (CTL), untersucht wurde, stellt aufgrund seiner Anwendungen in der Software- und Hardwareverifikation sowohl ein interessantes theoretisches als auch ein praktisch relevantes Problem dar. Diese Arbeit leistet einen Beitrag zur Untersuchung der rechnerischen Komplexität des Model Checking Problems für TEL. Zunächst wird die Komplexität von Elmc, dem Model Checking Problem der atemporalen Version EL von TEL, bestimmt und dann als Grundlage für die Bestimmung der Komplexität von Telmcf, dem Problem des Model Checkings für TEL über Spuren endlicher Länge, verwendet. Anschließend wird die Komplexität von Telmc, der Model Checking Problem für TEL über Spuren unendlicher Länge, untersucht. Es wird gezeigt, dass die Komplexität von Elmc und Telmcf coNP-vollständig ist, während die von Telmc Pspace-vollständig ist. Motiviert durch die Unlösbarkeit des Telmc-Problems werden einige seiner Fragmente analysiert, sowohl um rechnerisch einfachere Probleme zu entdecken als auch um festzustellen, wann die Unlösbarkeit beginnt. Es wird gezeigt, dass die Entscheidung über Telmc1 (das Fragment von Telmc, bei dem die sogenannte temporale Höhe durch 1begrenzt ist) und Telmc(○, U) (das Fragment von Telmc, bei dem nur die Operatoren ○ und U zulässig sind) coNP-vollständig ist, während die Entscheidung über Telmc(U, R) (das Telmc-Fragment, in dem nur die Operatoren U und R zulässig sind) und Telmc(○, R) (das Telmc-Fragment, in dem nur die Operatoren ○ und R zulässig sind) Pspace-vollständig ist. Als einfache Folge davon ist die Entscheidung über Telmc12, Telmc12(U, R) und Telmc12(○, R) ebenfalls Pspace-vollständig. Die Komplexität von Telts, einer Erweiterung des Model Checking Problems für TEL über sogenannte Transition Systems, wird ebenfalls untersucht. Telts ist in zwei Varianten unterteilt: Telts∀, die universelle Variante von Telts, und Telts∃, die existenzielle Variante. Die Entscheidung über Telts∀ ist nachweislich Pspace-vollständig, während die Entscheidung über Telts∃ Expspace-vollständig ist. Die Entscheidung von Telts∀(R) (dem Fragment des Telts∀-Problems, bei dem nur der Release Operator R zulässig ist) ist weiterhin Pspace-vollständig, und ebenso ist die Entscheidung von Telts∃(R) (dem Fragment des Telts∃-Problems, bei dem nur der Release Operator R zulässig ist) weiterhin Expspace-vollständig.

Given an LTL formula φ and a trace T, the problem of model checking for temporal equilibrium logic (TEL) is the problem of determining whether T is a temporal equilibrium model (TEM) of φ. The problem of model checking, already studied for several other prominent classical logics, like linear temporal logic (LTL) and computation tree logic (CTL), represents both an interesting theoretical problem and a practically relevant one, due to its applications in software and hardware verification. This work contributes to the study of the computational complexity of the model checking problem for TEL. The complexity of Elmc, the model checking problem of the atemporal version EL of TEL, is first determined and then used as a basis to determine the complexity of Telmcf, the problem of model checking for TEL over traces of finite length. The complexity of Telmc, model checking for TEL over traces of infinite length, is subsequently studied. The complexity of Elmc and Telmcf is shown to be coNP–complete, whereas the one of Telmc Pspace–complete. Motivated by the intractability of the Telmc problem, some of its fragments are analyzed, in the attempt to discover computationally easier problems and to determine when intractability starts to emerge. Deciding Telmc1 (the fragment of Telmc where the so-called temporal height is bounded by 1) and Telmc(○, U) (the fragment of Telmc where only the ○ and U operators are allowed) is shown to be coNP–complete, while deciding Telmc(U, R) (the Telmc fragment where only the U and R operators areallowed) and Telmc(○, R) (the Telmc fragment where only the ○ and R operators are allowed) Pspace–complete. As a simple corollary, deciding Telmc12, Telmc12(U, R) and Telmc12(○, R) is also Pspace–complete. The complexity of Telts, an extension of model checking for TEL over transition systems, is also investigated. Telts is divided into two variants, Telts∀, the universal variant of Telts, and Telts∃, the existential one. Deciding Telts∀ is shown to be Pspace–complete, whereas deciding Telts∃ Expspace–complete. Deciding Telts∀(R) (the fragment of the Telts∀ problem where only the release operator R is allowed) is still Pspace–complete, and similarly deciding Telts∃(R) (the fragment of the Telts∃ problem where only the release operator R is allowed) Expspace–complete.