Model checking properties on reduced trace systems

DOI10.3390/a7030339zbMath1461.68119OpenAlexW2081369054MaRDI QIDQ1736621

Antonella Santone, Gigliola Vaglini

Publication date: 26 March 2019

Published in: Algorithms (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.3390/a7030339

zbMATH Keywords

model checkinglinear temporal logicstate explosionbranching-time temporal logictrace systems

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Temporal logic (03B44)

Uses Software

• CADP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Improved model checking of hierarchical systems
• Linear temporal logic symbolic model checking
• Pushdown module checking
• Concurrent systems and inevitability
• Local model checking for infinite state spaces
• Symbolic model checking: \(10^{20}\) states and beyond
• The modal mu-calculus alternation hierarchy is strict
• Module checking
• Partial-order methods for the verification of concurrent systems. An approach to the state-explosion problem
• Computer aided verification. 8th international conference, CAV '96, New Brunswick, NJ, USA, July 31 -- August 3, 1996. Proceedings
• Pushdown module checking with imperfect information
• Selective mu-calculus and formula-based equivalence of transition systems
• Complexity results on branching-time pushdown model checking
• An expressively complete linear time temporal logic for Mazurkiewicz traces
• When not losing is better than winning: abstraction and refinement for the full \(\mu\)-calculus
• CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes
• LTL Generalized Model Checking Revisited
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Graph-Based Algorithms for Boolean Function Manipulation
• The complexity of propositional linear temporal logics
• TEMPORAL LOGICS FOR TRACE SYSTEMS: ON AUTOMATED VERIFICATION
• Poset properties of complex traces
• FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
• Pushdown Module Checking
• Algorithms for Omega-Regular Games with Imperfect Information
• 2-Visibly Pushdown Automata
• Mechanizing Mathematical Reasoning

This page was built for publication: Model checking properties on reduced trace systems