Extended full computation-tree logics for paraconsistent model checking
DOI:
https://doi.org/10.12775/LLP.2006.015Keywords
bisimulation, full computation-tree logic, location operator, paraconsistent model checkingAbstract
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.References
A. Almukdad and D. Nelson, “Constructible falsity and inexact predicates”, Journal of Symbolic Logic 49 (1984), 231–233.
S. Benferhat, D. Dubois, S. Kaci, and H. Prade, “Bipolar possibility theory in preference modeling: Representation, fusion and optimal solutions”, Information Fusion 7(1) (2006), 135–150.
J.-Y. Béziau, “The future of paraconsistent logic”, Logical Studies 2 (1999).
S. Bistarelli, M.S. Pini, F. Rossi, and K.B. Venable, “Positive and negative preferences”, Proceeding of the 7th International Workshop on Preferences and soft constraints (Soft 2005) held in conjunction with CP2005, Sitges, Spain, 2005.
G. Bruns and P. Godefroid, “Model checking with multi-valued logics”, Proceedings of ICALP2004, Lecture Notes in Computer Science 3142 (2004), pp. 281–293.
M.C. Browne, E.M. Clarke, and O. Grumberg, “Characterizing finite Kripke structures in propositional temporal logic”, Theoretical Computer Science 59 (1988), pp. 115–131.
W.A. Carnielli, M.E. Coniglio, and J. Marcos, “Logics of formal inconsistency”, in D. Gabbay and F. Guenthner (eds.), Handbook of Philosophical Logic, vol. 14, pp. 1–124, Kluwer Academic Publishers, 2004.
M. Chechik, B. Devereux, S. Easterbrook, and A. Gurfinkel, “Multi-valued symbolic model-checking”, ACM Transactions on Software Engineering and Methodology 12(4) (2004), 1–38.
M. Chechik, and W. MacCaull, “CTL model-checking over logics with non-classical negations”, Proceedings of 33rd IEEE International Conference on Multi-valued logics (ISMVL’03), pp. 293–300, 2003.
E.M. Clarke and E.A. Emerson, “Design and synthesis of synchronization skeletons using branching time temporal logic”, Proceedings of the Workshop on logic of Programs, Lecture Notes in Computer Science 131 (1981), 52–71.
E.M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, “Counterexample-guided abstraction refinement for symbolic model checking”, Journal of the ACM 50(5) (2003), 752–794.
E.M. Clarke, O. Grumberg, and D.A. Peled, Model checking, The MIT Press, 1999.
C.V. Damásio and L.M. Pereira, “A survey of paraconsistent semantics for logic programs”, in D. Gabbay and P. Smets (eds.), Handbook of Defeasible Reasoning and Uncertainty Management Systems, vol. 2, pp. 421–320, Kluwer Academic Publishers, 1998.
S. Easterbrook, and M. Chechik, “A framework for multi-valued reasoning over inconsistent viewpoints”, Proceedings of the 23rd International Conference on Software Engineering (ICSE 2001), pp. 411–420.
S. Easterbrook, and M. Chechik, “Automated paraconsistent reasoning via model cheking”, Proceedings of IJCAI Inconsistency Workshop, 8 pages, 2001.
E.A. Emerson and J.Y. Halpern, “‘Sometimes’ and ‘not never’ revisited: on branching versus linear time temporal logic”, Journal of the ACM 33(1) (1986), 151–178.
E.A. Emerson and P. Sistla, “Deciding full branching time logic”, Information and Control 61 (1984), 175–201.
Ken I. Fukuda, “Biomedical ontologies and their applications” (in Japanese), Journal of the Japanese Society for Artificial Intelligence 22(1) (2007), 70–76.
A. Gurfinkel, O. Wei, and M. Chechik, “Yasm: a software model-checker for verification and refutation”, Proceedings of Computer Aided Verification (CAV’06), pp. 170–174, 2006.
A. Gurfinkel, and M. Chechik, “Why wast a perfectly good abstraction?”, Proceedings of TACAS’06, Lecture Notes in Computer Science 3920 (2006), 212–226.
N. Kamide, “Gentzen-type methods for bilattice negation”, Studia Logica 80 (2005), 265–289.
N. Kamide, “A spatial modal logic with a location interpretation”, Mathematical Logic Quarterly 51(4) (2005), 331–341.
N. Kamide, “Linear and affine logics with temporal, spatial and epistemic operators”, Theoretical Computer Science 353(1–3) (2006), 165–207.
N. Kamide, “Foundations of paraconsistent resolution”, Fundamenta Informatica 71(4) (2006), 419–441.
N. Kobayashi, T. Shimizu, and A. Yonezawa, “Distributed concurrent linear logic programming”, Theoretical Computer Science 227 (1999), 185–220.
D. Nelson, “Constructible falsity”, Journal of Symbolic Logic 14 (1949), 16–26.
G. Priest, and R. Routly, “Introduction: paraconsistent logics”, Studia Logica 43 (1982), 3–16.
A. Pnueli, “The temporal logic of programs”, Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, pp. 46–57, 1977.
J.P. Quielle and J. Sifakis, “Specification and verification of concurrent systems in CESAR”, Proceedings of the 5th International Symposium on Programming, pp. 337–351, 1982.
R. Routley, “Semantical analysis of propositional systems of Fitch and Nelson”, Studia Logica 33 (1974), 283–298.
W. Rautenberg, Klassische und nicht-klassische Aussagenlogik, Vieweg, Braunschweig, 1979.
B. Smith, W. Ceusters, B. Klagges, J. Köhler, A. Kumar, J. Lomax, C. Mungall, F. Neuhaus, A.L. Rector, and C. Rosse, “Relations in biomedical ontologies”, Genome Biology 6 (2005), R46, 15 pages.
G. Wagner, “Logic programming with strong negation and inexact predicates”, Journal of Logic and Computation 1(6) (1991), 835–859.
H. Wansing, “The logic of information structures”, Lecture Notes in Artificial Intelligence 681 (1993), 163 pages.
Downloads
Published
How to Cite
Issue
Section
Stats
Number of views and downloads: 521
Number of citations: 0
