Bounded model checking for interval probabilistic timed graph transformation systems against properties of probabilistic metric temporal graph logic

DOI10.1016/J.JLAMP.2023.100938MaRDI QIDQ6151620zbMATH OpenFDO

Authors Sven Schneider, Maria Maximova, Holger Giese

Publication date 12 February 2024

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/J.JLAMP.2023.100938

zbMATH Keywords

bounded model checkingcyber-physical systemsprobabilistic timed systemsqualitative analysisquantitative analysis

Mathematics Subject Classification ID

Computer science (68-XX)

Cites work

• A brief account of runtime verification
• A compositional modelling and analysis framework for stochastic hybrid systems
• A framework for the verification of infinite-state graph transformation systems
• A logic for reasoning about time and reliability
• A simulator for probabilistic timed graph transformation systems with complex large-scale topologies
• A theory of timed automata
• Algorithms for monitoring real-time properties
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Automatic verification of real-time systems with discrete probability distributions.
• Bounded model checking for probabilistic programs
• Compositional analysis of probabilistic timed graph transformation systems
• Correctness of high-level transformation systems relative to nested conditions
• Efficient Runtime Verification of First-Order Temporal Properties
• Formal verification of invariants for attributed graph transformation systems based on nested attributed graph conditions
• Fundamentals of algebraic graph transformation
• Graph and model transformation. General framework and applications
• Graph Transformations
• scientific article; zbMATH DE number 1670788 (Why is no real title available?)
• scientific article; zbMATH DE number 1507210 (Why is no real title available?)
• scientific article; zbMATH DE number 1884410 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• scientific article; zbMATH DE number 3249395 (Why is no real title available?)
• Interval probabilistic timed graph transformation systems
• Invariant Analysis for Multi-agent Graph Transformation Systems Using k-Induction
• Lectures on Concurrency and Petri Nets
• Markov Chains
• Model checking probabilistic real-time properties for service-oriented systems with service level agreements
• Model-checking continuous-time Markov chains
• Monitoring metric first-order temporal properties
• Optimistic and pessimistic on-the-fly analysis for metric temporal graph logic
• Probabilistic automata
• Probabilistic graph transformation systems
• Probabilistic Metric Temporal Graph Logic
• Probabilistic timed graph transformation systems
• Stochastic graph transformation systems
• Symbolic graphs for attributed graph constraints
• Symbolic model checking for real-time systems
• The benefits of relaxing punctuality
• The benefits of relaxing punctuality
• The probabilistic model checking landscape
• Timed context-free temporal logics
• Timed temporal logics
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: Bounded model checking for interval probabilistic timed graph transformation systems against properties of probabilistic metric temporal graph logic

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