DocumentCode
1687618
Title
Towards symbolic strategy synthesis for <>-LTL
Author
Harding, Aidan ; Ryan, Mark ; Schobbens, Pierre-Yves
Author_Institution
Sch. of Comput. Sci., Birmingham Univ., UK
fYear
2003
Firstpage
137
Lastpage
146
Abstract
We provide a symbolic algorithm for synthesizing winning strategies in Alternating Time Temporal Logic. ATL has game semantics, which makes it suitable for modeling open systems where coalitions of agents work together to achieve their goals. A typical use of the algorithm would begin with a highly non-deterministic set of agents, A, for which we wish to synthesize behavior. These may be composed with a set of opponent agents, which provide an environment. The desired behavior is then written in <>-LTL, and a strategy for A to implement this is synthesized. If A implements this strategy, then the system will be guaranteed to satisfy the desired property. The algorithm presented here is part of a work in progress and updates can be found at http://www.cs.bham.ac.uk/ ∼ ath/atl_synthesis.
Keywords
formal specification; game theory; open systems; temporal logic; agent-based systems; alternating time temporal logic; game semantics; open systems; symbolic strategy synthesis; Artificial intelligence; Automata; Binary decision diagrams; Computer science; Encoding; Gold; History; Logic; Open systems; Prototypes;
fLanguage
English
Publisher
ieee
Conference_Titel
Temporal Representation and Reasoning, 2003 and Fourth International Conference on Temporal Logic. Proceedings. 10th International Symposium on
ISSN
1530-1311
Print_ISBN
0-7695-1912-1
Type
conf
DOI
10.1109/TIME.2003.1214889
Filename
1214889
Link To Document