scholarly journals Tableau-Like Automata-Based Axiomatization for Propositional Linear Temporal Logic

10.29007/df56 ◽  
2018 ◽  
Author(s):  
Nikolay V. Shilov
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Decision Procedure ◽  
Computer Programs ◽  
Linear Temporal Logic ◽  
Local Model ◽  
Specification And Verification ◽  
Local Model Checking

Propositional Linear Temporal Logic (PLTL) is a very popular formalism for specification and verification of computer programs and systems. This extended abstract sketches a tableau-like axiomatization for PLTL based on automata-theoretic decision procedure coupled with tableau for local model checking of the propositional μ-Calculus.

scholarly journals Local model checking for infinite state spaces

1992 ◽  
Vol 96 (1) ◽  
pp. 157-174 ◽  
Author(s):  
Julian Bradfield ◽  
Colin Stirling
Keyword(s):  
Model Checking ◽  
Local Model ◽  
State Spaces ◽  
Infinite State ◽  
Local Model Checking

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.

scholarly journals A Compositional Proof System for the Modal mu-Calculus

1998 ◽  
Vol 5 (40) ◽  
Author(s):  
Henrik Reif Andersen ◽  
Colin Stirling ◽  
Glynn Winskel
Keyword(s):  
Model Checking ◽  
Process Algebra ◽  
Local Model ◽  
Proof System ◽  
Compositional Reasoning ◽  
General Process ◽  
Finite State ◽  
Local Model Checking

We present a proof system for determining satisfaction between<br />processes in a fairly general process algebra and assertions of the modal mu-calculus. The proof system is compositional in the structure of processes. It extends earlier work on compositional reasoning within the modal mu-calculus and combines it with techniques from work on local model checking. The proof system is sound for all processes and complete for a class of finite-state processes.

scholarly journals Local Model Checking of Weighted CTL with Upper-Bound Constraints

2013 ◽  
pp. 178-195 ◽  
Author(s):  
Jonas Finnemann Jensen ◽  
Kim Guldstrand Larsen ◽  
Jiří Srba ◽  
Lars Kaerlund Oestergaard
Keyword(s):  
Model Checking ◽  
Upper Bound ◽  
Local Model ◽  
Bound Constraints ◽  
Weighted Ctl ◽  
Local Model Checking
Sign in / Sign up

Export Citation Format

Share Document