Many decision problems in formal verification and design can be suitably formulated in game-theoretic terms. This is the case for the model checking of open and closed systems and both controller and reactive synthesis. Interpreted in this context, these problems require one to find a strategy (i.e., a plan) to force the system to fulfill some desired goal, no matter what the opponent (e.g., the environment) does. A strategy essentially constrains the possible behaviors of the system to those that are compatible with the decisions dictated by the plan itself. Therefore, finding a strategy to meet some goal basically reduces to identifying a portion of the model of interest (i.e., one of its substructures) that satisfies that goal. In this view, the ability to reason about substructures becomes a crucial aspect for several fundamental problems. In this article, we present and study a new branching-time temporal logic, called Substructure Temporal Logic (STL * for short), whose distinctive feature is to allow for quantifying over the possible substructure of a given structure. The logic is obtained by adding four new temporal-like operators to CTL *, whose interpretation is given relative to the partial order induced by a suitable substructure relation. STL * turns out to be very expressive and allows one to capture in a very natural way many well-known problems, such as module checking, reactive synthesis, and reasoning about games in a wide sense. A formal account of the model-theoretic properties of the new logic and results about (un)decidability and complexity of related decision problems are also provided.

Reasoning about substructures and games / Benerecetti, Massimo; Mogavero, Fabio; Murano, Aniello. - In: ACM TRANSACTIONS ON COMPUTATIONAL LOGIC. - ISSN 1529-3785. - 16:3(2015), pp. 1-51. [10.1145/2757286]

Reasoning about substructures and games

BENERECETTI, MASSIMO;MOGAVERO, FABIO;MURANO, ANIELLO
2015

Abstract

Many decision problems in formal verification and design can be suitably formulated in game-theoretic terms. This is the case for the model checking of open and closed systems and both controller and reactive synthesis. Interpreted in this context, these problems require one to find a strategy (i.e., a plan) to force the system to fulfill some desired goal, no matter what the opponent (e.g., the environment) does. A strategy essentially constrains the possible behaviors of the system to those that are compatible with the decisions dictated by the plan itself. Therefore, finding a strategy to meet some goal basically reduces to identifying a portion of the model of interest (i.e., one of its substructures) that satisfies that goal. In this view, the ability to reason about substructures becomes a crucial aspect for several fundamental problems. In this article, we present and study a new branching-time temporal logic, called Substructure Temporal Logic (STL * for short), whose distinctive feature is to allow for quantifying over the possible substructure of a given structure. The logic is obtained by adding four new temporal-like operators to CTL *, whose interpretation is given relative to the partial order induced by a suitable substructure relation. STL * turns out to be very expressive and allows one to capture in a very natural way many well-known problems, such as module checking, reactive synthesis, and reasoning about games in a wide sense. A formal account of the model-theoretic properties of the new logic and results about (un)decidability and complexity of related decision problems are also provided.
2015
Reasoning about substructures and games / Benerecetti, Massimo; Mogavero, Fabio; Murano, Aniello. - In: ACM TRANSACTIONS ON COMPUTATIONAL LOGIC. - ISSN 1529-3785. - 16:3(2015), pp. 1-51. [10.1145/2757286]
File in questo prodotto:
File Dimensione Formato  
TOCL-post.pdf

solo utenti autorizzati

Tipologia: Documento in Post-print
Licenza: Accesso privato/ristretto
Dimensione 801.13 kB
Formato Adobe PDF
801.13 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11588/631289
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 11
  • ???jsp.display-item.citation.isi??? 6
social impact