NDLI: Reasoning About Substructures and Games

Content Provider	ACM Digital Library
Author	Murano, Aniello Benerecetti, Massimo Mogavero, Fabio
Copyright Year	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.
Starting Page	1
Ending Page	51
Page Count	51
File Format	PDF
ISSN	15293785
e-ISSN	1557945X
DOI	10.1145/2757286
Volume Number	16
Issue Number	3
Journal	ACM Transactions on Computational Logic (TOCL)
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2015-07-01
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Temporal logics Quantification on substructures Reasoning about games
Content Type	Text
Resource Type	Article
Subject	Theoretical Computer Science Logic Computational Mathematics Computer Science

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Qualitative concurrent parity games

Heterogeneous temporal probabilistic agents

Reasoning about actions with sensing under qualitative and probabilistic uncertainty

Deterministic generators and games for Ltl fragments

Calculus of cooperation and game-based reasoning about protocol privacy

Undecidable Propositional Bimodal Logics and One-Variable First-Order Linear Temporal Logics with Counting

Graded computation tree logic

Reasoning about evolving nonmonotonic knowledge bases

On the Decidability of Elementary Modal Logics

Reasoning About Substructures and Games

Similar Documents

Qualitative concurrent parity games

Heterogeneous temporal probabilistic agents

Reasoning about actions with sensing under qualitative and probabilistic uncertainty

Deterministic generators and games for Ltl fragments

Calculus of cooperation and game-based reasoning about protocol privacy

Undecidable Propositional Bimodal Logics and One-Variable First-Order Linear Temporal Logics with Counting

Graded computation tree logic

Reasoning about evolving nonmonotonic knowledge bases

On the Decidability of Elementary Modal Logics

Reasoning About Substructures and Games