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

DOI10.1016/j.jlamp.2023.100938MaRDI QIDQ6151620

Maria Maximova, Sven Schneider, Holger Giese

Publication date: 12 February 2024

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

zbMATH Keywords

quantitative analysisbounded model checkingcyber-physical systemsqualitative analysisprobabilistic timed systems

Mathematics Subject Classification ID

Computer science (68-XX)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Symbolic graphs for attributed graph constraints
• A framework for the verification of infinite-state graph transformation systems
• A theory of timed automata
• Symbolic model checking for real-time systems
• A logic for reasoning about time and reliability
• Automatic verification of real-time systems with discrete probability distributions.
• Algorithms for monitoring real-time properties
• Bounded model checking for probabilistic programs
• Probabilistic timed graph transformation systems
• Compositional analysis of probabilistic timed graph transformation systems
• Interval probabilistic timed graph transformation systems
• A compositional modelling and analysis framework for stochastic hybrid systems
• A brief account of runtime verification
• Fundamentals of algebraic graph transformation
• Graph and model transformation. General framework and applications
• Monitoring Metric First-Order Temporal Properties
• Probabilistic Graph Transformation Systems
• Correctness of high-level transformation systems relative to nested conditions
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Markov Chains
• The benefits of relaxing punctuality
• The Probabilistic Model Checking Landscape
• Formal Verification of Invariants for Attributed Graph Transformation Systems Based on Nested Attributed Graph Conditions
• Optimistic and Pessimistic On-the-fly Analysis for Metric Temporal Graph Logic
• A Simulator for Probabilistic Timed Graph Transformation Systems with Complex Large-Scale Topologies
• Timed Temporal Logics
• The benefits of relaxing punctuality
• Graph Transformations
• Probabilistic automata
• Lectures on Concurrency and Petri Nets
• Model-checking continuous-time Markov chains
• Efficient Runtime Verification of First-Order Temporal Properties
• 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