Alternating-time Temporal Logic

Alternating-time Temporal Logic was introduced in 1997 by Alur, Henzinger and Kupferman. Unlike traditional snapshot logic?s and earlier temporal logic?s, it allows the direct expression of responsibility to maintain constraint?s as commitments of multiple parties in cooperative relationships.

Technically, it is a variant of branching-time temporal logic? in which path quantifier?s are each replaced by a cooperation modality? - which assert?s that for each constraint there is a strategy profile? shared by some group to restore or maintain it when it ceases to be true, or it is perceived (not just by that group) that it will soon cease to be true.

For instance, a statement such as "bioregional divisions of party B named B1 and B2 can cooperate to ensure that party B does not enter a fail state" is expressed as

{{B1, B2}}nf~fail

Where nf is a temporal operator? meaning "now and forevermore?". Other temporal operators in ATL are:

wiki extension

In the living ontology and some large public wikis these relationships are expressed by naming conventions. An extension to the ATL model is the "as of" convention to signal information that is true now but is likely to change in future. Distinctions between observed, predicted, offered or request?ed behaviour are also not part of ATL but extend it to detail aspects of the relationship model itself.

cite Logic for Mechanism Design - a Manifesto Pauly, Wooldridge

cite Alur, Henzinger, Kupferman

cite Hubley

Show php error messages