scholarly journals Decision procedures and expressiveness in the temporal logic of branching time

1985 ◽  
Vol 30 (1) ◽  
pp. 1-24 ◽  
Author(s):  
E.Allen Emerson ◽  
Joseph Y. Halpern
Keyword(s):  
Temporal Logic ◽  
Decision Procedures ◽  
Branching Time

scholarly journals An axiomatization of full Computation Tree Logic

2001 ◽  
Vol 66 (3) ◽  
pp. 1011-1057 ◽  
Author(s):  
M. Reynolds
Keyword(s):  
Temporal Logic ◽  
Open Problem ◽  
Branching Time ◽  
Computation Tree Logic ◽  
Computation Tree ◽  
Complete Axiomatization

AbstractWe give a sound and complete axiomatization for the full computation tree logic. CTL*, of R-generable models. This solves a long standing open problem in branching time temporal logic.

scholarly journals Converging from branching to linear metrics on Markov chains

2017 ◽  
Vol 29 (1) ◽  
pp. 3-37 ◽  
Author(s):  
GIORGIO BACCI ◽  
GIOVANNI BACCI ◽  
KIM G. LARSEN ◽  
RADU MARDARE
Keyword(s):  
Model Checking ◽  
Markov Chains ◽  
Temporal Logic ◽  
Polynomial Time ◽  
Linear Time ◽  
Linear Temporal Logic ◽  
Np Hard ◽  
Branching Time ◽  
Threshold Problem ◽  
Ltl Model Checking

We study two well-known linear-time metrics on Markov chains (MCs), namely, the strong and strutter trace distances. Our interest in these metrics is motivated by their relation to the probabilistic linear temporal logic (LTL)-model checking problem: we prove that they correspond to the maximal differences in the probability of satisfying the same LTL and LTL−X(LTL without next operator) formulas, respectively.The threshold problem for these distances (whether their value exceeds a given threshold) is NP-hard and not known to be decidable. Nevertheless, we provide an approximation schema where each lower and upper approximant is computable in polynomial time in the size of the MC.The upper approximants are bisimilarity-like pseudometrics (hence, branching-time distances) that converge point-wise to the linear-time metrics. This convergence is interesting in itself, because it reveals a non-trivial relation between branching and linear-time metric-based semantics that does not hold in equivalence-based semantics.

A PROOF PROCEDURE FOR TEMPORAL LOGIC PROGRAMMING

2004 ◽  
Vol 15 (02) ◽  
pp. 417-443 ◽  
Author(s):  
MANOLIS GERGATSOULIS ◽  
CHRISTOS NOMIKOS
Keyword(s):  
Logic Programming ◽  
Programming Languages ◽  
Temporal Logic ◽  
Programming Language ◽  
Branching Time ◽  
Logic Programs ◽  
Temporal Logic Programming ◽  
Time Logic ◽  
Proof Procedure ◽  
Resolution Proof

In this paper, we propose a new resolution proof procedure for the branching-time logic programming language Cactus. The particular strength of the new proof procedure, called CSLD-resolution, is that it can handle, in a more general way, open-ended queries, i.e. goal clauses that include atoms which do not refer to specific moments in time, without the need of enumerating all their canonical instances. We also prove soundness, completeness and independence of the computation rule for CSLD-resolution. The new proof procedure overcomes the limitations of a family of proof procedures for temporal logic programming languages, which were based on the notions of canonical program and goal clauses. Moreover, it applies directly to Chronolog programs and it can be easily extended to apply to multi-dimensional logic programs as well as to Chronolog(MC) programs.

Sign in / Sign up

Export Citation Format

Share Document