Characterizing finite Kripke structures in propositional temporal logic
type: Item
instance of: scholarly article
title: Characterizing finite Kripke structures in propositional temporal logic
zbMATH Open document ID: 0677.03011
DOI: 10.1016/0304-3975(88)90098-9
author: M. C. Browne
author: Orna Grumberg
author: Edmund Clarke
published in: Theoretical Computer Science
publication date: 1988-01-01T00:00:00Z
review text: A (finite) Kripke structure is a triple \(M=<S,R,{\mathcal L}>\), where S is the (finite) set of states, \(R\subseteq S\times S\) is a (total) transition relation and \({\mathcal L}\) is a valuation from states to the set of subsets of atomic formulas of a given (propositional) temporal logic theory \({\mathcal T}\). The chosen logics are \(CTL^*\) [\textit{E. A. Emerson} and \textit{J. Y. Halpern}, J. Assoc. Comput. Mach. 33, 151-178 (1986; Zbl 0629.68020)] and CTL. CTL is a restricted subset of \(CTL^*\) that permits only branching time operators (linear time operator being disallowed) such that each path quantifier must be immediately followed by exactly one of the operators G (``always''), F (``sometimes''), X (``next time'') or U (``until''). It is shown that if two finite Kripke structures can be distinguished (via valid formulas) in \(CTL^*\), then they can also be distinguished in CTL. The formulas implied characterize the Kripke structures via a natural equivalence relation (similar to bisimulation), or via a ``stuttering'' relation (by eliminating the ``next time'' operator). A polynomial time algorithm for computing the equivalence relation via stuttering is also given.
Mathematics Subject Classification ID: 03B45
Mathematics Subject Classification ID: 03B70
Mathematics Subject Classification ID: 68Q65
Mathematics Subject Classification ID: 03C90
zbMATH DE Number: 4108726
zbMATH Keywords: branching time semantics
zbMATH Keywords: linear time semantics
zbMATH Keywords: Kripke structure
zbMATH Keywords: temporal logic
zbMATH Keywords: stuttering
reviewed by: Cristian Masalagiu
describes a project that uses: CESAR
MaRDI profile type: Publication
full work available at URL: 0304-3975(88)90098-9
OpenAlex ID: W1990183105
cites work: A linear algorithm to solve fixed-point equations on transition systems
cites work: The temporal logic of branching time
cites work: Automatic Verification of Sequential Circuits Using Temporal Logic
cites work: Q3336675
cites work: Automatic verification of finite-state concurrent systems using temporal logic specifications
cites work: Deciding full branching time logic
cites work: Q3690206
cites work: Q3883467
cites work: The power of the future perfect in program logics
cites work: A calculus of communicating systems
cites work: Hierarchical verification of asynchronous circuits using temporal logic
cites work: Synthesis of Communicating Processes from Temporal Logic Specifications
cites work: Q3694687
cites work: The complexity of propositional linear temporal logics
Recommended article: Augmenting branching temporal logics with existential quantification over atomic propositions
Recommended article: Q3028984
Recommended article: Q2970258
Recommended article: Computation Tree Logic with Deadlock Detection
Recommended article: A quantitative characterization of weighted Kripke structures in temporal logic
Recommended article: Q4475142
Recommended article: Logics and decidability for labelled pre- and partially ordered Kripke structures
Recommended article: Q4037127
Recommended article: Kripke incompleteness of first-order calculi with temporal modalities of CTL and near logics
Recommended article: Temporal logic CTL \(+\) Prolog
description: scientific article; zbMATH DE number 4108726