Alternating-time Temporal Logic

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

Technically, it is a variant of branching-time temporal logic in which path quantifiers are each replaced by a cooperation modality - which asserts 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 requested 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