Combined model checking for temporal, probabilistic, and real-time logics

DOI10.1016/J.TCS.2013.07.012MaRDI QIDQ407511zbMATH OpenOpenAlexWikidataFDO

Authors Savas Konur, Michael Fisher, Sven Schewe

Publication date 2 September 2014

Published in Theoretical Computer Science (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1016/j.tcs.2013.07.012

zbMATH Keywords

complexitymodel checkingmulti-agent systemsformal verificationcombination of logics

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Agent technology and artificial intelligence (68T42) Combined logics (03B62) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• A compositional automata-based approach for model checking multi-agent systems
• Specification and Verification of Multi-Agent Systems
• Logic Programming
• scientific article; zbMATH DE number 2215634
• scientific article; zbMATH DE number 1202873

Cites work

• scientific article; zbMATH DE number 1215478 (Why is no real title available?)
• scientific article; zbMATH DE number 1142326 (Why is no real title available?)
• scientific article; zbMATH DE number 1989659 (Why is no real title available?)
• scientific article; zbMATH DE number 2046116 (Why is no real title available?)
• scientific article; zbMATH DE number 2064229 (Why is no real title available?)
• scientific article; zbMATH DE number 1500666 (Why is no real title available?)
• scientific article; zbMATH DE number 2087624 (Why is no real title available?)
• scientific article; zbMATH DE number 795590 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• A theory of timed automata
• Adding a temporal dimension to a logic system
• Automatic verification of real-time systems with discrete probability distributions.
• Bounded model checking for knowledge and real time
• Combinations of modal logics
• Combining temporal logic systems
• Completeness and decidability of tense logics closely related to logics above K4
• Computer Aided Verification
• Cooperation, knowledge, and time: Alternating-time temporal epistemic logic and its applications
• Handbook of modal logic
• Many-dimensional modal logics: theory and applications
• Mobile ambients
• Model checking of probabilistic and nondeterministic systems
• Model-checking in dense real-time
• Specifying and reasoning about uncertain agents
• Strict Divergence for Probabilistic Timed Automata
• The product of converse PDL and polymodal K
• Why combine logics?

Cited in

(11)

• A compositional automata-based approach for model checking multi-agent systems
• Verification of heterogeneous multi-agent system using MCMAS
• Multi-agent verification and control with probabilistic model checking
• Formal verification of multi-agent systems behaviour emerging from cognitive task analysis
• IPL: an integration property language for multi-model cyber-physical systems
• Dynamic logic assigned to automata
• Towards light-weight probabilistic model checking
• Temporal Logic Trees for Model Checking and Control Synthesis of Uncertain Discrete-Time Systems
• scientific article; zbMATH DE number 7319046 (Why is no real title available?)
• When human intuition fails: using formal methods to find an error in the ``proof of a multi-agent protocol
• Credible futures

Describes a project that uses

Uses Software

• PRISM
• MCK

This page was built for publication: Combined model checking for temporal, probabilistic, and real-time logics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q407511)