You have just completed your registration at OpenAire.
Before you can login to the site, you will need to activate your account.
An e-mail will be sent to you with the proper instructions.
Important!
Please note that this site is currently undergoing Beta testing.
Any new content you create is not guaranteed to be present to the final version
of the site upon release.
Alternating Time Temporal Logic (ATL) is widely used for the verification of multi-agent systems. We consider Resource Agent Logic (RAL), which extends ATL to allow the verification of properties of systems where agents act under resource constraints. The model checking problem for RAL with unbounded production and consumption of resources is known to be undecidable. We review existing (un)decidability results for fragments of RAL, tighten some existing undecidability results, and identify several aspects which affect decidability of model checking. One of these aspects is the availability of a ‘do nothing’, or idle action, which does not produce or consume resources. Analysis of undecidability results allows us to identify a significant new fragment of RAL for which model checking is decidable.
[1] N. Alechina, B. Logan, H. N. Nguyen, A. Rakib, A logic for coalitions with bounded resources, in: C. Boutilier (Ed.), Proceedings of the Twenty First International Joint Conference on Artificial Intelligence (IJCAI 2009), Vol. 2, AAAI Press, 2009, pp. 659-664.
[2] N. Bulling, B. Farwer, On the (un-)decidability of model checking resource-bounded agents, in: H. Coelho, R. Studer, M. Wooldridge (Eds.), Proceedings of the 19th European Conference on Artificial Intelligence (ECAI 2010), IOS Press, 2010, pp. 567-572.
[6] N. Alechina, B. Logan, H. N. Nguyen, F. Raimondi, Decidable model-checking for a resource logic with production of resources, in: T. Schaub, G. Friedrich, B. O'Sullivan (Eds.), Proceedings of the 21st European Conference on Artificial Intelligence (ECAI-2014), IOS Press, 2014, pp. 9-14.
[8] N. Alechina, B. Logan, H. N. Nguyen, F. Raimondi, Model-checking for resource-bounded ATL with production and consumption of resources, Journal of Computer and System Sciences(in press).
[11] M. Pauly, A modal logic for coalitional power in games, Journal of Logic and Computation 12 (1) (2002) 149-166.
[12] N. Alechina, B. Logan, H. N. Nguyen, A. Rakib, Logic for coalitions with bounded resources, Journal of Logic and Computation 21 (6) (2011) 907-937.
[13] M. Z. Kwiatkowska, G. Norman, D. Parker, Prism 4.0: Verification of probabilistic real-time systems, in: Proceedings of the 23rd International Conference on Computer Aided Verification (CAV 2011), Vol. 6806 of Lecture Notes in Computer Science, Springer, 2011, pp. 585-591.
[14] N. Bulling, B. Farwer, Expressing properties of resource-bounded systems: The logics RBTL and RBTL∗, in: Computational Logic in MultiAgent Systems - 10th International Workshop, CLIMA X, Revised Selected and Invited Papers, Vol. 6214 of Lecture Notes in Computer Science, 2010, pp. 22-45.
[15] D. Della Monica, M. Napoli, M. Parente, On a logic for coalitional games with priced-resource agents, Electronic Notes in Theoretical Computer Science 278 (2011) 215-228.
[16] D. Della Monica, G. Lenzi, On a priced resource-bounded alternating μ-calculus, in: J. Filipe, A. L. N. Fred (Eds.), Proceedings of the 4th International Conference on Agents and Artificial Intelligence (ICAART 2012), SciTePress, 2012, pp. 222-227.
[17] J. Daniel, A. Cimatti, A. Griggio, S. Tonetta, S. Mover, Infinite-state liveness-to-safety via implicit abstraction and well-founded relations, in: S. Chaudhuri, A. Farzan (Eds.), Proceedings of the 28th International Conference on Computer Aided Verification (CAV 2016), Vol. 9779 of Lecture Notes in Computer Science, Springer, 2016, pp. 271-291.
[18] B. Cook, H. Khlaaf, N. Piterman, On automation of CTL* verification for infinite-state systems, in: D. Kroening, C. S. Pasareanu (Eds.), Proceedings of the 27th International Conference on Computer Aided Verification (CAV 2015), Vol. 9206 of Lecture Notes in Computer Science, Springer, 2015, pp. 13-29.
[21] B. Cook, E. Koskinen, M. Y. Vardi, Temporal property verification as a program analysis task - extended version, Formal Methods in System Design 41 (1) (2012) 66-82.
[22] M. Fisher, L. A. Dennis, M. P. Webster, Verifying autonomous systems, Communications of the ACM 56 (9) (2013) 84-93.
[24] J. Esparza, Decidability and complexity of Petri net problems - an introduction, in: Lectures on Petri Nets I: Basic Models, Vol. 1491 of Lecture Notes in Computer Science, Springer-Verlag, 1998, pp. 374-428.
[26] D. Porello, N. Troquard, A resource-sensitive account of the use of artifacts, in: A. L. C. Bazzan, M. N. Huhns, A. Lomuscio, P. Scerri (Eds.), Proceedings of the 13th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS 2014), IFAAMAS/ACM, 2014, pp. 1549-1550.
[27] D. Porello, N. Troquard, A resource-sensitive logic of agency, in: T. Schaub, G. Friedrich, B. O'Sullivan (Eds.), Proceedings of the 21st European Conference on Artificial Intelligence (ECAI 2014), IOS Press, 2014, pp. 723-728.
[28] P. W. O'Hearn, D. J. Pym, The logic of bunched implications, Bulletin of Symbolic Logic 5 (02) (1999) 215-244.
[30] J. Brotherston, C. Calcagno, Classical BI: a logic for reasoning about dualising resources, in: Z. Shao, B. C. Pierce (Eds.), Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2009), ACM, 2009, pp. 328-339.
[31] M. Collinson, B. Monahan, D. J. Pym, A logical and computational theory of located resource, Journal of Logic and Compututation 19 (6) (2009) 1207-1244.
[32] R. Alur, T. A. Henzinger, O. Kupferman, Alternating-time temporal logic, Journal of the ACM 49 (5) (2002) 672-713.
[33] J. E. Hopcroft, J. D. Ullman, Introduction to Automata Theory, Languages, and Computation, Addison-Wesley, 1979.
[34] J. L. Peterson, Petri net theory and the modeling of systems, Prentice Hall Englewood Cliffs (NJ), 1981.