Abstract
Will the cost for observing additional real-world phenomena in a world model be recovered by the resulting increase in the quality of the implementations based on the model? We address the quest for optimal models in light of industrial practices in systems engineering, where the development of control strategies is based on combined models of a system and its environment. We introduce the notion of remorsefree dominance between strategies, where one strategy is preferred over another if it outperforms the other strategy in comparable situations, even if neither strategy is guaranteed to achieve all objectives. We call a world model optimal if it is sufficiently precise to allow for a remorsefree dominating strategy that is guaranteed to remain dominant even if the world model is refined. We present algorithms for the automatic verification and synthesis of dominant strategies, based on tree automata constructions from reactive synthesis.
This research was partially supported by the German Science Foundation within the Transregional Collaborative Research Center TR14 AVACS.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proc. of POPL, pp. 179–190 (1989)
Kupferman, O., Vardi, M.Y.: Synthesis with incomplete informatio. In: Proc. of ICTL (1997)
Finkbeiner, B., Schewe, S.: Uniform distributed synthesis. In: Proc. of LICS, pp. 321–330 (2005)
Piterman, N., Pnueli, A., Sa’ar, Y.: Synthesis of reactive(1) designs. In: Proc. of VMCAI, pp. 364–380 (2006)
Finkbeiner, B., Schewe, S.: SMT-based synthesis of distributed systems. In: Proc. of AFM (2007)
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, New York (1991)
Grädel, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games. LNCS, vol. 2500. Springer, Heidelberg (2002)
Vardi, M.Y., Wilke, T.: Automata: from logics to algorithms. In: Flum, J., Grädel, E., Wilke, T. (eds.) Logic and Automata: History and Perspectives, pp. 629–736 (2007)
Jurdziński, M.: Small progress measures for solving parity games. In: Proc. STACS, pp. 290–301 (2000)
Loomes, G., Sugden, R.: Regret theory: An alternative theory of rational choice under uncertainty. Economic Journal 92, 805–824 (1982)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Damm, W., Finkbeiner, B. (2011). Does It Pay to Extend the Perimeter of a World Model?. In: Butler, M., Schulte, W. (eds) FM 2011: Formal Methods. FM 2011. Lecture Notes in Computer Science, vol 6664. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-21437-0_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-21437-0_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-21436-3
Online ISBN: 978-3-642-21437-0
eBook Packages: Computer ScienceComputer Science (R0)