An axiomatization of full Computation Tree Logic

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.

Download Full-text

The temporal logic of coalgebras via Galois algebras

Mathematical Structures in Computer Science ◽

10.1017/s096012950200378x ◽

2002 ◽

Vol 12 (6) ◽

pp. 875-903 ◽

Cited By ~ 13

Author(s):

BART JACOBS

Keyword(s):

State Space ◽

Temporal Logic ◽

Metric Spaces ◽

Linear Temporal Logic ◽

The State ◽

Temporal Logics ◽

Computation Tree Logic ◽

Computation Tree ◽

Polynomial Functors

This paper introduces a temporal logic for coalgebras. Nexttime and lasttime operators are defined for a coalgebra, acting on predicates on the state space. They give rise to what is called a Galois algebra. Galois algebras form models of temporal logics like Linear Temporal Logic (LTL) and Computation Tree Logic (CTL). The mapping from coalgebras to Galois algebras turns out to be functorial, yielding indexed categorical structures. This construction gives many examples, for coalgebras of polynomial functors on sets. More generally, it will be shown how ‘fuzzy’ predicates on metric spaces, and predicates on presheaves, yield indexed Galois algebras, in basically the same coalgebraic manner.

Download Full-text

Logical foundations of hierarchical model checking

Data Technologies and Applications ◽

10.1108/dta-01-2018-0002 ◽

2018 ◽

Vol 52 (4) ◽

pp. 539-563 ◽

Cited By ~ 1

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.

Download Full-text

QUANTUM COMPUTATION TREE LOGIC — MODEL CHECKING AND COMPLETE CALCULUS

International Journal of Quantum Information ◽

10.1142/s0219749908003530 ◽

2008 ◽

Vol 06 (02) ◽

pp. 219-236 ◽

Cited By ~ 17

Author(s):

P. BALTAZAR ◽

R. CHADHA ◽

P. MATEUS

Keyword(s):

Model Checking ◽

Quantum Computation ◽

Propositional Logic ◽

Key Distribution ◽

Logic Model ◽

Quantum States ◽

Computation Tree Logic ◽

Computation Tree ◽

Complete Axiomatization ◽

Logic Model Checking

Logics for reasoning about quantum states and their evolution have been given in the literature. In this paper, we consider quantum computation tree logic (QCTL), which adds temporal modalities to exogenous quantum propositional logic. We give a sound and complete axiomatization of QCTL and combine the standard CTL model-checking algorithm with the dEQPL model-checking algorithm to obtain a model-checking algorithm for QCTL. Finally, we illustrate the use of the logic by reasoning about the BB84 key distribution protocol.

Download Full-text

Theorem Proving for Pointwise Metric Temporal Logic Over the Naturals via Translations

Journal of Automated Reasoning ◽

10.1007/s10817-020-09541-4 ◽

2020 ◽

Vol 64 (8) ◽

pp. 1553-1610

Author(s):

Ullrich Hustadt ◽

Ana Ozaki ◽

Clare Dixon

Keyword(s):

Temporal Logic ◽

Traffic Management ◽

Monotonic Function ◽

The Other ◽

Branching Time ◽

Metric Temporal Logic ◽

Time Points ◽

Computation Tree ◽

Better Than ◽

Time Point

Abstract We study translations from metric temporal logic (MTL) over the natural numbers to linear temporal logic (LTL). In particular, we present two approaches for translating from MTL to LTL which preserve the complexity of the satisfiability problem for MTL. In each of these approaches we consider the case where the mapping between states and time points is given by (i) a strict monotonic function and by (ii) a non-strict monotonic function (which allows multiple states to be mapped to the same time point). We use this logic to model examples from robotics, traffic management, and scheduling, discussing the effects of different modelling choices. Our translations allow us to utilise LTL solvers to solve satisfiability and we empirically compare the translations, showing in which cases one performs better than the other. We also define a branching-time version of the logic and provide translations into computation tree logic.

Download Full-text