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

DOI10.1016/J.TCS.2013.07.012zbMATH Open1360.68591OpenAlexW2060551079WikidataQ98283457 ScholiaQ98283457MaRDI QIDQ407511FDOQ407511

Authors: Savas Konur, Michael Fisher, Sven Schewe 

Publication date: 2 September 2014

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

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

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

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)

Cites Work

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

Cited In (11)

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

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)