CTL* model checking for data-aware dynamic systems with arithmetic

DOI10.1007/978-3-031-10769-6_4OpenAlexW4289104017MaRDI QIDQ2104496FDOQ2104496

Authors: Paolo Felli, Marco Montali, Sarah Winkler 

Publication date: 7 December 2022

Full work available at URL: https://arxiv.org/abs/2205.08976

zbMATH Keywords

verificationconstraintsSMTCTL*counter systems

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• An automata-theoretic approach to constraint LTL
• Process-centric views of data-driven business artifacts
• Satisfiability of \(\operatorname{ECTL}^\ast\) with constraints
• Balanced multi-perspective checking of process conformance
• Deciding properties of integral relational automata
• An automata-based approach for \(\text{CTL}^{*}\) with constraints
• Branching-Time Temporal Logic Extended with Qualitative Presburger Constraints
• Verification of qualitative \(\mathbb Z\) constraints
• Title not available (Why is that?)
• Model-checking \(\mathrm{CTL}^*\) over flat Presburger counter systems
• First-order \(\mu\)-calculus over generic transition systems and applications to the situation calculus
• Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems
• Iterating Octagons
• Decision procedures. An algorithmic point of view
• Title not available (Why is that?)
• LTL over integer periodicity constraints
• Cover Algorithms and Their Combination
• Title not available (Why is that?)
• Soundness verification of data-aware process models with variable-to-variable conditions
• Model-checking graded computation-tree logic with finite path semantics
• Verification of gap-order constraint abstractions of counter systems
• Equivalence between model-checking flat counter systems and Presburger arithmetic
• Branching-time model checking gap-order constraint systems

Cited In (1)

• Communicating Sequential Processes. The First 25 Years

Uses Software

• PNML
• z3
• CVC4

This page was built for publication: CTL* model checking for data-aware dynamic systems with arithmetic

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