A decision procedure for combinations of propositional temporal logic and other specialized theories

1986 ◽  
Vol 2 (2) ◽  
pp. 171-190 ◽  
Author(s):  
David A. Plaisted
Keyword(s):  
Temporal Logic ◽  
Decision Procedure

An Automata-Theoretic Decision Procedure for Propositional Temporal Logic with Since and Until1

1992 ◽  
Vol 17 (3) ◽  
pp. 271-282
Author(s):  
Y.S. Ramakrishna ◽  
L.E. Moser ◽  
L.K. Dillon ◽  
P.M. Melliar-Smith ◽  
G. Kutty
Keyword(s):  
Temporal Logic ◽  
Decision Procedure ◽  
Linear Time ◽  
Computer Systems ◽  
Hierarchical Abstraction ◽  
Soundness And Completeness

We present an automata-theoretic decision procedure for Since/Until Temporal Logic (SUTL), a linear-time propositional temporal logic with strong non-strict since and until operators. The logic, which is intended for specifying and reasoning about computer systems, employs neither next nor previous operators. Such operators obstruct the use of hierarchical abstraction and refinement and make reasoning about concurrency difficult. A proof of the soundness and completeness of the decision procedure is given, and its complexity is analyzed.

Algorithm for Decision Procedure in Temporal Logic Treating Uncertainty, Plausibility, Knowledge and Interacting Agents

2012 ◽  
pp. 32-46
Author(s):  
V. Rybakov
Keyword(s):  
Normal Form ◽  
Temporal Logic ◽  
Decision Procedure ◽  
Linear Temporal Logic ◽  
Satisfiability Problem ◽  
Global Knowledge ◽  
Interacting Agents ◽  
Logical Operations ◽  
Multi Agent ◽  
Bounded Size

Our paper studies a logic UIALTL, which is a combination of the linear temporal logic LTL, a multi-agent logic with operation for passing knowledge via agents’ interaction, and a suggested logic based on operation of logical uncertainty. The logical operations of UIALTL also include (together with operations from LTL) operations of strong and weak until, agents’ knowledge operations, operation of knowledge via interaction, operation of logical uncertainty, the operations for environmental and global knowledge. UIALTL is defined as a set of all formulas valid at all Kripke-Hintikka like models NC. Any frame NC represents possible unbounded (in time) computation with multi-processors (parallel computational units) and agents’ channels for connections between computational units. The main aim of our paper is to determine possible ways for computation logical laws of UIALTL. Principal problems we are dealing with are decidability and the satisfiability problems for UIALTL. We find an algorithm which recognizes theorems of UIALTL (so we show that UIALTL is decidable) and solves satisfiability problem for UIALTL. As an instrument we use reduction of formulas to rules in the reduced normal form and a technique to contract models NC to special non-UIALTL-models, and, then, verification of validity these rules in models of bounded size. The paper uses standard results from non-classical logics based on Kripke-Hintikka models.

A decision procedure for propositional projection temporal logic with infinite models

2007 ◽  
Vol 45 (1) ◽  
pp. 43-78 ◽  
Author(s):  
Zhenhua Duan ◽  
Cong Tian ◽  
Li Zhang
Keyword(s):  
Temporal Logic ◽  
Decision Procedure

Efficient decision procedure for propositional projection temporal logic

2020 ◽  
Vol 838 ◽  
pp. 1-16
Author(s):  
Xinfeng Shu ◽  
Nan Zhang ◽  
Xiaobing Wang ◽  
Liang Zhao
Keyword(s):  
Temporal Logic ◽  
Decision Procedure

A decision procedure and complete axiomatization for projection temporal logic

2020 ◽  
Vol 819 ◽  
pp. 50-84 ◽  
Author(s):  
Xinfeng Shu ◽  
Zhenhua Duan ◽  
Hongwei Du
Keyword(s):  
Temporal Logic ◽  
Decision Procedure ◽  
Complete Axiomatization

scholarly journals Restrictions for loop-check in sequent calculus for temporal logic

2008 ◽  
Vol 48 ◽  
Author(s):  
Adomas Birštunas
Keyword(s):  
Temporal Logic ◽  
Decision Procedure ◽  
Sequent Calculus ◽  
Linear Temporal Logic ◽  
Derivation Tree

In this paper, we present sequent calculus for linear temporal logic. This sequent calculus uses efficient loop-check techinque. We prove that we can use not all but only several special sequents from the derivation tree for the loop-check. We use indexes to discover these special sequents in the sequent calculus. These restrictions let us to get efficient decision procedure based on introduced sequent calculus.

scholarly journals Restrictions for loop-check in sequent calculus for temporal logic with until operator

2009 ◽  
Vol 50 ◽  
Author(s):  
Adomas Birštunas
Keyword(s):  
Temporal Logic ◽  
Decision Procedure ◽  
Sequent Calculus ◽  
Derivation Tree ◽  
Branching Time

In this paper, we present sequent calculus for branching-time temporal logic with until operator. This sequent calculus uses efficient loop-checktechinque. We prove that we can use not all but only several special sequents from the derivation tree for the loop-check. We use indexes to discover these special sequents in the sequent calculus. These restrictions let us to get efficient decision procedure based on introduced sequent calculus.

Sign in / Sign up

Export Citation Format

Share Document