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 :
https://search.ricest.ac.ir/dl/search/defaultta.aspx?DTC=49&DC=1687618
بازگشت