scholarly journals Branching time regular temporal logic for model checking with linear time complexity

2005 ◽  
pp. 253-262 ◽  
Author(s):  
Kiyoharu Hamaguchi ◽  
Hiromi Hiraishi ◽  
Shuzo Yajima
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Time Complexity ◽  
Linear Time ◽  
Branching Time

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.

Logical foundations of hierarchical model checking

2018 ◽  
Vol 52 (4) ◽  
pp. 539-563 ◽  
Author(s):  
Norihiro Kamide
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Hierarchical Model ◽  
Design Methodology ◽  
Linear Time ◽  
Hierarchical Systems ◽  
Content Type ◽  
Computation Tree Logic ◽  
Computation Tree ◽  
Linear Time Temporal Logic

Purpose The purpose of this paper is to develop new simple logics and translations for hierarchical model checking. Hierarchical model checking is a model-checking paradigm that can appropriately verify systems with hierarchical information and structures. Design/methodology/approach In this study, logics and translations for hierarchical model checking are developed based on linear-time temporal logic (LTL), computation-tree logic (CTL) and full computation-tree logic (CTL*). A sequential linear-time temporal logic (sLTL), a sequential computation-tree logic (sCTL), and a sequential full computation-tree logic (sCTL*), which can suitably represent hierarchical information and structures, are developed by extending LTL, CTL and CTL*, respectively. Translations from sLTL, sCTL and sCTL* into LTL, CTL and CTL*, respectively, are defined, and theorems for embedding sLTL, sCTL and sCTL* into LTL, CTL and CTL*, respectively, are proved using these translations. Findings These embedding theorems allow us to reuse the standard LTL-, CTL-, and CTL*-based model-checking algorithms to verify hierarchical systems that are modeled and specified by sLTL, sCTL and sCTL*. Originality/value The new logics sLTL, sCTL and sCTL* and their translations are developed, and some illustrative examples of hierarchical model checking are presented based on these logics and translations.

scholarly journals REASONING ABOUT TRANSFINITE SEQUENCES

2007 ◽  
Vol 18 (01) ◽  
pp. 87-112 ◽  
Author(s):  
STÉPHANE DEMRI ◽  
DAVID NOWAK
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Linear Time ◽  
Temporal Logics ◽  
Future Time ◽  
New Class ◽  
Linear Time Temporal Logic ◽  
Do So ◽  
Time Operators

We introduce a family of temporal logics to specify the behavior of systems with Zeno behaviors. We extend linear-time temporal logic LTL to authorize models admitting Zeno sequences of actions and quantitative temporal operators indexed by ordinals replace the standard next-time and until future-time operators. Our aim is to control such systems by designing controllers that safely work on ω-sequences but interact synchronously with the system in order to restrict their behaviors. We show that the satisfiability and model-checking for the logics working on ωk-sequences is EXPSPACE-complete when the integers are represented in binary, and PSPACE-complete with a unary representation. To do so, we substantially extend standard results about LTL by introducing a new class of succinct ordinal automata that can encode the interaction between the different quantitative temporal operators.

A LOGIC BASED APPROACH TO PLANNING FOR SPECIFYING A CLASS OF TEMPORALLY EXTENDED GOALS

2004 ◽  
Vol 13 (03) ◽  
pp. 469-485 ◽  
Author(s):  
RAJDEEP NIYOGI
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Polynomial Time ◽  
Linear Temporal Logic ◽  
The Other ◽  
Logical Framework ◽  
Branching Time ◽  
Optimal Plan ◽  
Other Hand ◽  
Planning Procedure

Planning with temporally extended goals has recently been the focus of much attention to researchers in the planning community. We study a class of planning goals where in addition to a main goal there exist other goals, which we call auxiliary goals, that act as constraints to the main goal. Both these type of goals can, in general, be a temporally extended goal. Linear temporal logic (LTL) is inadequate for specification of the overall goals of this type, although, for some situations, it is capable of expressing them separately. A branching-time temporal logic, like CTL, on the other hand, can be used for specifying these goals. However, we are interested in situations where an auxiliary goal has to be satisfiable within a fixed bound. We show that CTL becomes inadequate for capturing these situations. We bring out an existing logic, called min-max CTL, and show how it can effectively be used for the planning purpose. We give a logical framework for expressing the overall planning goals. We propose a sound and complete planning procedure that incorporates a model checking technology. Doing so, we can answer such planning queries as plan existence at the onset besides producing an optimal plan (if any) in polynomial time.

scholarly journals On the Satisfiability and Model Checking for one Parameterized Extension of Linear-time Temporal Logic

2021 ◽  
Vol 28 (4) ◽  
pp. 356-371
Author(s):  
Anton Romanovich Gnatenko ◽  
Vladimir Anatolyevich Zakharov
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Linear Time ◽  
Complete Solution ◽  
Reactive Systems ◽  
Expressive Power ◽  
Regular Languages ◽  
Specification Languages ◽  
Temporal Logics ◽  
Emptiness Problem

Sequential reactive systems are computer programs or hardware devices which process the flows of input data or control signals and output the streams of instructions or responses. When designing such systems one needs formal specification languages capable of expressing the relationships between the input and output flows. Previously, we introduced a family of such specification languages based on temporal logics $LTL$, $CTL$ and $CTL^*$ combined with regular languages. A characteristic feature of these new extensions of conventional temporal logics is that temporal operators and basic predicates are parameterized by regular languages. In our early papers, we estimated the expressive power of the new temporal logic $Reg$-$LTL$ and introduced a model checking algorithm for $Reg$-$LTL$, $Reg$-$CTL$, and $Reg$-$CTL^*$. The main issue which still remains unclear is the complexity of decision problems for these logics. In the paper, we give a complete solution to satisfiability checking and model checking problems for $Reg$-$LTL$ and prove that both problems are Pspace-complete. The computational hardness of the problems under consideration is easily proved by reducing to them the intersection emptyness problem for the families of regular languages. The main result of the paper is an algorithm for reducing the satisfiability of checking $Reg$-$LTL$ formulas to the emptiness problem for Buchi automata of relatively small size and a description of a technique that allows one to check the emptiness of the obtained automata within space polynomial of the size of input formulas.

scholarly journals Parallel Model Checking Algorithms for Linear-Time Temporal Logic

2018 ◽  
pp. 457-507 ◽  
Author(s):  
Jiri Barnat ◽  
Vincent Bloemen ◽  
Alexandre Duret-Lutz ◽  
Alfons Laarman ◽  
Laure Petrucci ◽  
...  
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Linear Time ◽  
Parallel Model ◽  
Linear Time Temporal Logic

scholarly journals Undecidability of QLTL with two variables and one monadic predicate letter

2021 ◽  
Vol 27 (2) ◽  
pp. 93-120
Author(s):  
Dmitry Shkatov ◽  
Mikhail Rybakov
Keyword(s):  
Temporal Logic ◽  
Linear Time ◽  
Satisfiability Problem ◽  
Branching Time ◽  
Tiling Problem ◽  
Recursively Enumerable ◽  
Unlimited Supply ◽  
Domain Semantics ◽  
Linear Time Temporal Logic ◽  
Individual Variables

We study the algorithmic properties of the quantified linear-time temporal logic QLTL in languages with restrictions on the number of individual variables as well as the number and arity of predicate letters. We prove that the satisfiability problem for QLTL in languages with two individual variables and one monadic predicate letter in Σ 11 -hard. Thus, QLTL is Π 11 -hard, and so not recursively enumerable, in such languages. The resultholds both for the increasing domain and the constant domain semantics and is obtained by reduction from a Σ 11 -hard N×N recurrent tiling problem. It follows from the proof for QLTL that similar results hold for the quantified branching-time temporal logic QCTL, and hence for the quantified alternating-time temporal logic QATL. The result presented in this paper strengthens a result by I. Hodkinson, F. Wolter, and M. Zakharyaschev, who have shown that the satisfiability problem for QLTL is Σ 11 -hard in languages with two individual variablesand an unlimited supply of monadic predicate letters.

Sign in / Sign up

Export Citation Format

Share Document