Extended full computation-tree logics for paraconsistent model checking

Logic and Logical Philosophy 15 (3):251-276 (2007)
  Copy   BIBTEX

Abstract

It is known that the full computation-tree logic CTL * is an important base logic for model checking. The bisimulation theorem for CTL* is known to be useful for abstraction in model checking. In this paper, the bisimulation theorems for two paraconsistent four-valued extensions 4CTL* and 4LCTL* of CTL* are shown, and a translation from 4CTL* into CTL* is presented. By using 4CTL* and 4LCTL*, inconsistency-tolerant and spatiotemporal reasoning can be expressed as a model checking framework

Categories

Keywords

Reprint years

DOI

10.12775/llp.2006.015

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,386

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Model checking techniqes for the analysis of reactive systems.Stephan Merz - 2002 - Synthese 133 (1-2):173 - 201.
An axiomatization of full computation tree logic.M. Reynolds - 2001 - Journal of Symbolic Logic 66 (3):1011-1057.
Model checking for hybrid logic.Martin Lange - 2009 - Journal of Logic, Language and Information 18 (4):465-491.
ZF and the axiom of choice in some paraconsistent set theories.Thierry Libert - 2003 - Logic and Logical Philosophy 11:91-114.
Symbolic model checking of logics with actions.Charles Pecheur & Franco Raimondi - 2007 - In A. Lomuscio & S. Edelkamp (eds.), Model Checking and Artificial Intelligence. Springer. pp. 113--128.
Distributed extended beam search for quantitative model checking.Anton J. Wijs & Bert Lisser - 2007 - In A. Lomuscio & S. Edelkamp (eds.), Model Checking and Artificial Intelligence. Springer. pp. 166--184.
The complexity of hybrid logics over equivalence relations.Martin Mundhenk & Thomas Schneider - 2009 - Journal of Logic, Language and Information 18 (4):493-514.
Timed Modal Logics for Real-Time Systems: Specification, Verification and Control.Patricia Bouyer, Franck Cassez & François Laroussinie - 2011 - Journal of Logic, Language and Information 20 (2):169-203.
A framework for model checking institutions.Francesco Vigano - 2007 - In A. Lomuscio & S. Edelkamp (eds.), Model Checking and Artificial Intelligence. Springer. pp. 129--145.
A Symbolic Model Checking Framework for Safety Analysis, Diagnosis, and Synthesis.Piergiorgio Bertoli, Marco Bozzano & Alessandro Cimatti - 2007 - In A. Lomuscio & S. Edelkamp (eds.), Model Checking and Artificial Intelligence. Springer. pp. 1--18.
Polyadic dynamic logics for hpsg parsing.Anders Søgaard & Martin Lange - 2009 - Journal of Logic, Language and Information 18 (2):159-198.
Real-time model checking on secondary storage.Stefan Edelkamp & Shahid Jabbar - 2007 - In A. Lomuscio & S. Edelkamp (eds.), Model Checking and Artificial Intelligence. Springer. pp. 67--83.
Scientific Theories of Computational Systems in Model Checking.Nicola Angius & Guglielmo Tamburrini - 2011 - Minds and Machines 21 (2):323-336.
Idempotent Full Paraconsistent Negations are not Algebraizable.Jean- Yves Beziau - unknown

Analytics

Added to PP
2013-11-24

Downloads
34 (#458,553)

6 months
4 (#790,687)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

Constructible falsity.David Nelson - 1949 - Journal of Symbolic Logic 14 (1):16-26.
Constructible falsity and inexact predicates.Ahmad Almukdad & David Nelson - 1984 - Journal of Symbolic Logic 49 (1):231-233.
Constructible Falsity.David Nelson - 1950 - Journal of Symbolic Logic 15 (3):228-228.

View all 10 references / Add more references