On Probabilistic Computation Tree Logic

2004 ◽  
pp. 147-188 ◽  
Author(s):  
Frank Ciesinski ◽  
Marcus Größer
Keyword(s):  
Probabilistic Computation ◽  
Computation Tree Logic ◽  
Computation Tree

Bounded Model Checking for Probabilistic Computation Tree Logic

2012 ◽  
Vol 23 (7) ◽  
pp. 1656-1668 ◽  
Author(s):  
Cong-Hua ZHOU ◽  
Zhi-Feng LIU ◽  
Chang-Da WANG
Keyword(s):  
Model Checking ◽  
Bounded Model Checking ◽  
Probabilistic Computation ◽  
Computation Tree Logic ◽  
Computation Tree

scholarly journals Exogenous Probabilistic Computation Tree Logic

2007 ◽  
Vol 190 (3) ◽  
pp. 95-110 ◽  
Author(s):  
Pedro Baltazar ◽  
Paulo Mateus ◽  
Rajagopal Nagarajan ◽  
Nikolaos Papanikolaou
Keyword(s):  
Probabilistic Computation ◽  
Computation Tree Logic ◽  
Computation Tree

Polytime model checking for timed probabilistic computation tree logic

1998 ◽  
Vol 35 (8) ◽  
pp. 645-664 ◽  
Author(s):  
Danièle Beauquier ◽  
Anatol Slissenko
Keyword(s):  
Model Checking ◽  
Probabilistic Computation ◽  
Computation Tree Logic ◽  
Computation Tree

Method for Combining Paraconsistency and Probability in Temporal Reasoning

2016 ◽  
Vol 20 (5) ◽  
pp. 813-827 ◽  
Author(s):  
Norihiro Kamide ◽  
◽  
Daiki Koizumi ◽  
Keyword(s):  
Model Checking ◽  
Temporal Reasoning ◽  
Concurrent Systems ◽  
Embedding Theorem ◽  
Temporal Logics ◽  
Probabilistic Computation ◽  
Computation Tree Logic ◽  
Computation Tree

Computation tree logic (CTL) is known to be one of the most useful temporal logics for verifying concurrent systems by model checking technologies. However, CTL is not sufficient for handling inconsistency-tolerant and probabilistic accounts of concurrent systems. In this paper, a paraconsistent (or inconsistency-tolerant) probabilistic computation tree logic (PpCTL) is derived from an existing probabilistic computation tree logic (pCTL) by adding a paraconsistent negation connective. A theorem for embedding PpCTL into pCTL is proven, thereby indicating that we can reuse existing pCTL-based model checking algorithms. A relative decidability theorem for PpCTL, wherein the decidability of pCTL implies that of PpCTL, is proven using this embedding theorem. Some illustrative examples involving the use of PpCTL are also presented.

scholarly journals The temporal logic of coalgebras via Galois algebras

2002 ◽  
Vol 12 (6) ◽  
pp. 875-903 ◽  
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.

Sign in / Sign up

Export Citation Format

Share Document