Synthesizing agent protocols from LTL specifications against multiple partially-observable environments

作者: Alessio Lomuscio , Paolo Felli , Giuseppe De Giacomo

DOI:

关键词: Bounded functionTheoretical computer scienceComputer scienceObservableAlgorithmProtocol (object-oriented programming)

摘要: We consider the problem of synthesizing an agent protocol satisfying LTL specifications for multiple, partially-observable environments. present a sound and complete procedure solving synthesis in this setting show it is computationally optimal from theoretical complexity standpoint. While produces perfect-recall, hence unbounded, strategies we how to transform these into protocols with bounded number states.

参考文章(22)
Yuxiao Hu, Giuseppe De Giacomo, Generalized planning: synthesizing plans that work for multiple environments international joint conference on artificial intelligence. pp. 918- 923 ,(2011) , 10.5591/978-1-57735-516-8/IJCAI11-159
Joost-Pieter Katoen, Christel Baier, Principles of Model Checking (Representation and Mind Series) The MIT Press. ,(2008)
Blai Bonet, Héctor Geffner, Solving POMDPs: RTDP-bel vs. point-based algorithms international joint conference on artificial intelligence. pp. 1641- 1646 ,(2009)
Orna Kupfermant, Moshe Y. Vardit, Synthesis with Incomplete Informatio Springer, Dordrecht. pp. 109- 127 ,(2000) , 10.1007/978-94-015-9586-5_6
Ron van der Meyden, Finite State Implementations of Knowledge-Based Programs foundations of software technology and theoretical computer science. pp. 262- 273 ,(1996) , 10.1007/3-540-62034-6_55
Peter Gammie, Ron van der Meyden, MCK: Model Checking the Logic of Knowledge Computer Aided Verification. ,vol. 3114, pp. 479- 483 ,(2004) , 10.1007/978-3-540-27813-9_41
Moshe Y. Vardi, An automata-theoretic approach to linear temporal logic Proceedings of the VIII Banff Higher order workshop conference on Logics for concurrency : structure versus automata: structure versus automata. pp. 238- 266 ,(1996) , 10.1007/3-540-60915-6_6
Aidan Harding, Mark Ryan, Pierre-Yves Schobbens, A New Algorithm for Strategy Synthesis in LTL Games Tools and Algorithms for the Construction and Analysis of Systems. pp. 477- 492 ,(2005) , 10.1007/978-3-540-31980-1_31
Giuseppe De Giacomo, Moshe Y. Vardi, Automata-Theoretic Approach to Planning for Temporally Extended Goals Lecture Notes in Computer Science. pp. 226- 238 ,(1999) , 10.1007/10720246_18
Cindy Eisner, Dana Fisman, John Havlicek, Yoad Lustig, Anthony McIsaac, David Van Campenhout, Reasoning with Temporal Logic on Truncated Paths computer aided verification. pp. 27- 39 ,(2003) , 10.1007/978-3-540-45069-6_3