scientific article; zbMATH DE number 7439738

MaRDI QIDQ5015276zbMATH OpenFDO

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

Publication date 7 December 2021

Full work available at URL http://eptcs.web.cse.unsw.edu.au/paper.cgi?GandALF2016.12

Mathematics Subject Classification ID

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

Recommendations

• Cycle detection in computation tree logic
• scientific article; zbMATH DE number 7649967
• Computation tree logic with deadlock detection
• Loop detection by logically constrained term rewriting
• Verification, Model Checking, and Abstract Interpretation
• On inductive inference of cyclic structures
• A new approach to incremental cycle detection and related problems
• On the detection of some loops in recursive computations
• scientific article; zbMATH DE number 7155168
• Cyclic proofs of program termination in separation logic

Cites work

• \textit{Once} and \textit{for all}
• Alternating-time temporal logic
• An automata-theoretic approach to branching-time model checking
• Automata, logics, and infinite games. A guide to current research
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Decision procedures and expressiveness in the temporal logic of branching time
• Deterministic generators and games for LTL fragments
• Enriched MU-Calculi Module Checking
• Finitary winning in \({\omega}\)-regular games
• From liveness to promptness
• scientific article; zbMATH DE number 3870578 (Why is no real title available?)
• scientific article; zbMATH DE number 1223729 (Why is no real title available?)
• scientific article; zbMATH DE number 1980931 (Why is no real title available?)
• scientific article; zbMATH DE number 3212004 (Why is no real title available?)
• Infinite games on finitely coloured graphs with applications to automata on infinite trees
• Module checking
• On promptness in parity games
• Pushdown module checking
• Reasoning about strategies: on the model-checking problem
• Temporal logic can be more expressive
• The Complexity of Enriched Mu-Calculi
• TYPENESS FOR ω-REGULAR AUTOMATA
• “Sometimes” and “not never” revisited

Cited in

(4)

• An automata-theoretic approach to the verification of distributed algorithms
• Cycle detection in computation tree logic
• Computation tree logic for synchronization properties
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication:

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