Abstract
This paper studies the logic of modalities for motivational attitudes (desires, obligations, wishes, wants, intentions, etc.) that come with a deadline condition. For instance, an agent may want to get home before it starts raining. We use a ‘reduction approach’ from deontic logic to characterize two separate semantic definitions for these motivational modalities in CTL. The main advantage of applying reductions is that the formal reasoning can be performed entirely in CTL. We claim that the reduction approach applies to any motivational modality.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Anderson, A.R.: A reduction of deontic logic to alethic modal logic. Mind 67, 100–103 (1958)
Bolotov, A., Fisher, M.: A clausal resolution method for CTL branching-time temporal logic. Journal of Experimental and Theoretical Artificial Intelligence 11(1), 77–93 (1999)
Broersen, J.M.: Action negation and alternative reductions for dynamic deontic logics. Journal of Applied Logic 2(1), 153–168 (2003)
Broersen, J.M., Dignum, F., Dignum, V., Meyer, J.-J.: Designing a deontic logic of deadlines. In: Lomuscio, A., Nute, D. (eds.) DEON 2004. LNCS (LNAI), vol. 3065, pp. 43–56. Springer, Heidelberg (2004)
Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finitestate concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems 8(2) (1986)
Clarke, E.M., Grumberg, O., Long, D.: Verification tools for finite-state concurrent systems. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) REX 1993. LNCS, vol. 803, pp. 124–175. Springer, Heidelberg (1994)
Cohen, P.R., Levesque, H.J.: Intention is choice with commitment. Artificial Intelligence 42(3), 213–261 (1990)
Dignum, F., Broersen, J., Dignum, V., Meyer, J.-J.: Meeting the deadline: Why, when and how. In: Hinchey, M.G., Rash, J.L., Truszkowski, W.F., Rouff, C.A. (eds.) FAABS 2004. LNCS (LNAI), vol. 3228, pp. 30–40. Springer, Heidelberg (2004) (to appear)
Dignum, F., Kuiper, R.: Combining dynamic deontic logic and temporal logic for the specification of deadlines. In: Sprague Jr., R. (ed.) Proceedings of thirtieth HICSS (1997)
Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science. Formal Models and Semantics, ch. 14, vol. B, pp. 996–1072. Elsevier Science, Amsterdam (1990)
Kanger, S.: New foundations for ethical theory. In: Hilpinen, R. (ed.) Deontic Logic: Introductory and Systematic Readings, pp. 36–58. D. Reidel Publishing Company, Dordrecht (1971)
Lindström, S., Rabinowicz, W.: Unlimited doxastic logic for introspective agents. Erkenntnis 50, 353–385 (1999)
Meyer, J.-J.C.: A different approach to deontic logic: Deontic logic viewed as a variant of dynamic logic. Notre Dame Journal of Formal Logic 29, 109–136 (1988)
Meyer, J.-J.C., van der Hoek, W., van Linder, B.: A logical approach to the dynamics of commitments. Artificial Intelligence (1999)
Pratt, V.R.: Semantical considerations on Floyd-Hoare logic. In: Proceedings 17th IEEE Symposium on the Foundations of Computer Science, pp. 109–121. IEEE Computer Society Press, Los Alamitos (1976)
Rao, A.S., Georgeff, M.P.: Modeling rational agents within a BDI-architecture. In: Allen, J., Fikes, R., Sandewall, E. (eds.) Proceedings of the 2nd International Conference on Principles of Knowledge Representation and Reasoning (KR 1991), pp. 473–484. Morgan Kaufmann Publishers, San Francisco (1991)
Schild, K.: On the relationship between BDI-logics and standard logics of concurrency. Autonomous agents and multi-agent systems 3, 259–283 (2000)
Schnoebelen, P.: The complexity of temporal logic model checking. In: Balbiani, P., Suzuki, N.-Y., Wolter, F., Zakharyaschev, M. (eds.) Advances in Modal Logic, vol. 4, pp. 393–436 (2003)
Shankar, N.: Machine-assisted verification using theorem proving and model checking. In: Broy, M. (ed.) Mathematical Methods in Program Development, Springer, Heidelberg (1997)
von Wright, G.H.: Deontic logic. Mind 60, 1–15 (1951)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Broersen, J. (2004). On the Logic of ‘Being Motivated to Achieve ρ, Before δ’. In: Alferes, J.J., Leite, J. (eds) Logics in Artificial Intelligence. JELIA 2004. Lecture Notes in Computer Science(), vol 3229. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30227-8_29
Download citation
DOI: https://doi.org/10.1007/978-3-540-30227-8_29
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23242-1
Online ISBN: 978-3-540-30227-8
eBook Packages: Springer Book Archive