- New
-
Topics
- All Categories
- Metaphysics and Epistemology
- Value Theory
- Science, Logic, and Mathematics
- Science, Logic, and Mathematics
- Logic and Philosophy of Logic
- Philosophy of Biology
- Philosophy of Cognitive Science
- Philosophy of Computing and Information
- Philosophy of Mathematics
- Philosophy of Physical Science
- Philosophy of Social Science
- Philosophy of Probability
- General Philosophy of Science
- Philosophy of Science, Misc
- History of Western Philosophy
- Philosophical Traditions
- Philosophy, Misc
- Other Academic Areas
- Journals
- Submit material
- More
Model checking techniqes for the analysis of reactive systems
Synthese 133 (1):173 - 201 (2002)
Abstract
Model checking is a widely used technique that aids in the designand debugging of reactive systems. This paper gives an overview onthe theory and algorithms used for model checking, with a biastowards automata-theoretic approaches and linear-time temporallogic. We also describe elementary abstraction techniques useful forlarge systems that cannot be directly handled by model checking.Other Versions
No versions found
My notes
Similar books and articles
A Sat-Based Approach to Unbounded Model Checking for Alternating-Time Temporal Epistemic Logic.M. Kacprzak & W. Penczek - 2004 - Synthese 142 (2):203-227.
Checking EMTLK Properties of Timed Interpreted Systems Via Bounded Model Checking.Bożena Woźna-Szcześniak & Andrzej Zbrzezny - 2016 - Studia Logica 104 (4):641-678.
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.
Scientific Theories of Computational Systems in Model Checking.Nicola Angius & Guglielmo Tamburrini - 2011 - Minds and Machines 21 (2):323-336.
Bounded model checking real-time multi-agent systems with clock differences: theory and implementation.Alessio Lomuscio, Bożena Woźna & Andrzej Zbrzezny - 2007 - In A. Lomuscio & S. Edelkamp, Model Checking and Artificial Intelligence. Springer. pp. 95--112.
Model checking lattices: using and reasoning about information orders for abstraction.S. Hazelhurst & C. Seger - 1999 - Logic Journal of the IGPL 7 (3):375-411.
Extended full computation-tree logics for paraconsistent model checking.Norihiro Kamide - 2007 - Logic and Logical Philosophy 15 (3):251-276.
Formal Modelling and Verification of Probabilistic Resource Bounded Agents.Hoang Nga Nguyen & Abdur Rakib - 2023 - Journal of Logic, Language and Information 32 (5):829-859.
Model checking distributed temporal logic.Francisco Dionísio, Jaime Ramos, Fernando Subtil & Luca Viganò - forthcoming - Logic Journal of the IGPL.
Bisimulation, modal logic and model checking games.C. Stirling - 1999 - Logic Journal of the IGPL 7 (1):103-124.
Analytics
Added to PP
2009-01-28
Downloads
138 (#317,631)
6 months
14 (#866,120)
2009-01-28
Downloads
138 (#317,631)
6 months
14 (#866,120)
Historical graph of downloads
References found in this work
The Temporal Logic of Reactive and Concurrent Systems: Specifications.Zohar Manna & Amir Pnueli - 1992 - Springer Verlag.
Modal and Temporal Logics.Colin Stirling - 1991 - LFCS, Department of Computer Science, University of Edinburgh.
Try MATCHA Writer if you're interested in citing directly from PhilPapers and certifying your authorship.
This site uses cookies and Google Analytics (see our terms & conditions for details regarding the privacy implications). Use of this site is subject to terms & conditions.
All rights reserved by The PhilPapers Foundation