Proving feature non-interaction with alternating-time temporal logic

MaRDI QIDQ4817052zbMATH OpenFDO

Authors Franck Cassez, M. D. Ryan, Pierre Yves Schobbens

Publication date 14 September 2004

zbMATH Keywords

alternating transition systemalternating-time temporal logicbranching temporal logicfeature interactionreactive systems

Mathematics Subject Classification ID

Temporal logic (03B44) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Applications of game theory (91A80)

Recommendations

• Alternating-time temporal logic
• Time, knowledge, and cooperation: Alternating-time temporal epistemic logic and its applications
• Cooperation, knowledge, and time: Alternating-time temporal epistemic logic and its applications
• Time, knowledge, and cooperation: Alternating-time temporal epistemic logic and its applications
• On the Expressiveness and Complexity of ATL

Cited in

(2)

• Proving ATL* Properties of Infinite-State Systems
• Alternating-time temporal logic in the calculus of (co)inductive constructions

Describes a project that uses

Uses Software

• MOCHA

This page was built for publication: Proving feature non-interaction with alternating-time temporal logic

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