Cycle detection in computation tree logic

DOI10.1016/j.ic.2018.09.007zbMath1400.68123arXiv1609.04095OpenAlexW2962715492MaRDI QIDQ1784962

Giuseppe Perelli, Gaëlle Fontaine, Loredana Sorrentino, Fabio Mogavero, Aniello Murano

Publication date: 27 September 2018

Published in: Information and Computation (Search for Journal in Brave)

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

zbMATH Keywords

verificationmodel checkingtemporal logicsatisfiability

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• \textit{Once} and \textit{for all}
• Pushdown module checking
• From liveness to promptness
• Infinite games on finitely coloured graphs with applications to automata on infinite trees
• Module checking
• Automata, logics, and infinite games. A guide to current research
• Decision procedures and expressiveness in the temporal logic of branching time
• On Promptness in Parity Games*†
• Finitary winning in ω-regular games
• Reasoning About Strategies
• Temporal logic can be more expressive
• Alternating-time temporal logic
• Enriched MU-Calculi Module Checking
• The Complexity of Enriched Mu-Calculi
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• “Sometimes” and “not never” revisited
• Deterministic generators and games for Ltl fragments
• An automata-theoretic approach to branching-time model checking
• TYPENESS FOR ω-REGULAR AUTOMATA

This page was built for publication: Cycle detection in computation tree logic