Model-checking for ability-based logics with constrained plans
Article No.: 707, Pages 6305 - 6312
Abstract
We investigate the complexity of the model-checking problem for a family of modal logics capturing the notion of "knowing how". We consider the most standard ability-based knowing how logic, for which we show that modelchecking is PSpace-complete. By contrast, a multi-agent variant based on an uncertainty relation between plans in which uncertainty is encoded by a regular language, is shown to admit a PTime model-checking problem. We extend with budgets the above-mentioned ability-logics, as done for ATL-like logics. We show that for the former logic enriched with budgets, the complexity increases to at least ExpSpace-hardness, whereas for the latter, the PTime bound is preserved. Other variant logics are discussed along the paper.
References
[1]
Alechina, N.; Bulling, N.; Demri, S.; and Logan, B. 2018. On the Complexity of Resource-Bounded Logics. Theoretical Computer Science, 750: 69-100.
[2]
Alechina, N.; Bulling, N.; Logan, B.; and Nguyen, H. 2017. The virtues of idleness: A decidable fragment of resource agent logic. Artificial Intelligence, 245: 56-85.
[3]
Alur, R.; Henzinger, T.; and Kupferman, O. 2002. Alternating-time temporal logic. Journal of the ACM, 49(5): 672-713.
[4]
Areces, C.; Fervari, R.; Saravia, A.; and Velázquez-Quesada, F. 2021. Uncertainty-Based Semantics for Multi-Agent Knowing How Logics. In TARK'21, volume 335 of EPTCS, 23-37.
[5]
Blackburn, P.; de Rijke, M.; and Venema, Y. 2001. Modal Logic. Cambridge University Press.
[6]
Bouyer, P.; Fahrenberg, U.; Larsen, K.; Markey, N.; and Srba, J. 2008. Infinite Runs in Weighted Timed Automata with Energy Constraints. In FORMATS'08, volume 5215 of LNCS, 33-47. Springer.
[7]
Bulling, N.; and Goranko, V. 2022. Combining quantitative and qualitative reasoning in concurrent multi-player games. Autonomous Agents and Multi-Agent Systems, 36(2): 1-33.
[8]
Cao, R.; and Naumov, P. 2017. Budget-Constrained Dynamics in Multiagent Systems. In IJCAI'17, 915-921. ijcai.org.
[9]
Chatterjee, K.; Doyen, L.; and Henzinger, T. 2017. The Cost of Exactness in Quantitative Reachability. In Models, Algorithms, Logics and Tools - Essays Dedicated to Kim Guld-strand Larsen on the Occasion of His 60th Birthday, volume 10460 of LNCS, 367-381. Springer.
[10]
Cormen, T.; Leiserson, C.; Rivest, R. L.; and Stein, C. 2022. Introduction to Algorithms, 4th Edition. MIT Press.
[11]
Demri, S.; Goranko, V.; and Lange, M. 2016. Temporal Logics in Computer Science. Cambridge University Press.
[12]
Fervari, R.; Herzig, A.; Li, Y.; and Wang, Y. 2017. Strategically knowing how. In IJCAI'17, 1031-1038.ijcai.org.
[13]
Galil, Z. 1976. Hierarchies of complete problems. Acta Informatica, 6: 77-88.
[14]
Herzig, A. 2015. Logics of knowledge and action: critical analysis and challenges. Autonomous Agents and Multi Agent Systems, 29(5): 719-753.
[15]
Herzig, A.; and Troquard, N. 2006. Knowing how to play: uniform choices in logics of agency. In AAMAS'06, 209-216. ACM.
[16]
Jamroga, W.; and Ågotnes, T. 2007. Constructive knowledge: what agents can achieve under imperfect information. Journal of Applied Non Classical Logics, 17(4): 423-475.
[17]
Karp, R. M.; and Miller, R. E. 1969. Parallel Program Schemata. JCSS, 3(2): 147-195.
[18]
Kozen, D. 1977. Lower Bounds for Natural Proof Systems. In FOCS'77, 254-266. IEEE Computer Society.
[19]
Li, Y. 2017. Knowing what to do: a logical approach to planning ad knowing how. Ph.D. thesis, University of Groningen.
[20]
Li, Y.; and Wang, Y. 2017. Achieving While Maintaining: - A Logic of Knowing How with Intermediate Constraints. In ICLA'17, volume 10119 of LNCS, 154-167. Springer.
[21]
Li, Y.; and Wang, Y. 2021a. Knowing How to Plan. In TARK'21, volume 335 of EPTCS, 233-247.
[22]
Li, Y.; and Wang, Y. 2021b. Planning-based knowing how: A unified approach. Artificial Intelligence, 296: 103487.
[23]
Li, Y.; Yu, Q.; and Wang, Y. 2017. More for free: a dynamic epistemic framework for conformant planning over transition systems. JLC, 27(8): 2383-2410.
[24]
Lipton, R. 1976. The Reachability Problem Requires Exponential Space. Technical Report 62, Department of Computer Science, Yale University.
[25]
Naumov, P.; and Tao, J. 2018a. Second-Order Know-How Strategies. In AAMAS'18, 390-398.
[26]
Naumov, P.; and Tao, J. 2018b. Strategic Coalitions With Perfect Recall. In AAAI'18, 4702-4709. AAAI Press.
[27]
Naumov, P.; and Tao, J. 2018c. Together we know how to achieve: An epistemic logic of know-how. Artificial Intelligence, 262: 279-300.
[28]
Rackoff, C. 1978. The covering and boundedness problems for vector addition systems. Theoretical Computer Science, 6(2): 223-231.
[29]
Savitch, W. 1970. Relationships between nondeterministic and deterministic tape complexities. JCSS, 4(2): 177-192.
[30]
Smith, D.; and Weld, D. 1998. Conformant Graphplan. In AAAI'98, 889-896. AAAI Press / The MIT Press.
[31]
van der Hoek, W.; and Lomuscio, A. 2003. Ignore at your peril - towards a logic for ignorance. In AAMAS'03, 1148-1149. ACM.
[32]
van Ditmarsch, H.; Halpern, J.; van der Hoek, W.; and Kooi, B., eds. 2015. Handbook of Epistemic Logic. College Pub.
[33]
Wang, Y. 2015. A Logic of Knowing How. In LORI'15, volume 9394 of LNCS, 392-405. Springer.
[34]
Wang, Y. 2018a. Beyond knowing that: a new generation of epistemic logics. In van Ditmarsch, H.; and Sandu, G., eds., Jaakko Hintikka on knowledge and game theoretical semantics, 499-533. Springer.
[35]
Wang, Y. 2018b. A logic of goal-directed knowing how. Synthese, 195(10): 4419-4439.
Recommendations
Intuitionistic Trilattice Logics
We take up a suggestion by Odintsov (2009, Studia Logica, 91, 407–428) and define intuitionistic variants of certain logics arising from the trilattice SIXTEEN3 introduced in Shramko and Wansing (2005, Journal of Philosophical Logic, 34, 121–153 and ...
Multi-valued Modal Fixed Point Logics for Model Checking
ISMVL '09: Proceedings of the 2009 39th International Symposium on Multiple-Valued LogicIn this paper, I will show how multi-valued logics are used for model checking. Model checking is an automatic technique to analyze correctness of hardware and software systems. A model checker is based on a temporal logic or a modal fixed point logic. ...
Logics and translations for hierarchical model checking
In this study, logics and translations for hierarchical model checking are developed based on linear-time temporal logic (LTL) and computation-tree logic (CTL). Hierarchical model checking is a model checking paradigm that can appropriately verify ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © 2023 Association for the Advancement of Artificial Intelligence.
Sponsors
- Association for the Advancement of Artificial Intelligence
Publisher
AAAI Press
Publication History
Published: 07 February 2023
Qualifiers
- Research-article
- Research
- Refereed limited
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 14 Feb 2025