×

A dynamic deontic logic for complex contracts. (English) Zbl 1258.03024

This paper presents a dynamic deontic logic for contracts, not only software contracts, web services, etc., but especially legal contracts. This affects the design of the system. Distinctive here is its stance of the ought-to-do, whereby deontic modalities apply to complex actions, rather than propositions as in so much of deontic logic. In addition, each modality is indexed by a clause indicating a reparation in case of violation. Further, the deontic modalities are added to a dynamic logic in order to allow reasoning about sequences of actions, and also synchronous actions. Unlike other dynamic logics, this considers deterministic actions.
In addition to the formal analysis and representation of the applicable concepts, the principal result here is to establish that the deontic modalities over synchronous actions have the tree model property, and hence are decidable. Further, many familiar properties of the deontic modalities are indicated, as well as how the present system avoids many of the standard paradoxes of deontic logic.

MSC:

03B45 Modal logic (including the logic of norms)
03B25 Decidability of theories and sets of sentences

Software:

CLAN; Esterel
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Baader, F.; Nipkow, T., Term Rewriting and All That (1998), Cambridge University Press
[2] Ben-Ari, M.; Halpern, J. Y.; Pnueli, A., Finite models for deterministic propositional dynamic logic, (Even, S.; Kariv, O., Eighth Colloquium on Automata, Languages and Programming (ICALP’81). Eighth Colloquium on Automata, Languages and Programming (ICALP’81), LNCS, vol. 115 (1981), Springer), 249-263
[3] Berry, G., The foundations of Esterel, (Proof, Language, and Interaction: Essays in Honour of Robin Milner (2000), MIT Press), 425-454
[4] Blackburn, P.; de Rijke, M.; Venema, Y., Modal logic, Cambridge Tracts in Theoretical Computer Science, vol. 53 (2001), Cambridge University Press · Zbl 0988.03006
[5] J. Broersen, Modal Action Logics for Reasoning about Reactive Systems, Ph.D. Thesis, Vrije Universiteit Amsterdam, 2003.; J. Broersen, Modal Action Logics for Reasoning about Reactive Systems, Ph.D. Thesis, Vrije Universiteit Amsterdam, 2003.
[6] Broersen, J.; Wieringa, R.; Meyer, J.-J. C., A fixed-point characterization of a deontic logic of regular action, Fund. Inform., 48, 2-3, 107-128 (2001) · Zbl 0995.03016
[7] Bursuc, S.; Prisacariu, C., Unification and matching in separable theories (extended abstract), (Fernandez, M., 24th International Workshop on Unification (UNIF10) (2010), Edimburg: Edimburg UK)
[8] S. Bursuc, C. Prisacariu, Unification and Matching in Separable Theories - Technicalities, Tech. Rep. 398, Department of Informatics, University of Oslo, Norway, July 2010.; S. Bursuc, C. Prisacariu, Unification and Matching in Separable Theories - Technicalities, Tech. Rep. 398, Department of Informatics, University of Oslo, Norway, July 2010.
[9] Carmo, J.; Jones, A., Deontic logic and contrary-to-duties, (Gabbay, D.; Guenthner, F., Handbook of Philosophical Logic (2002), Kluwer Academic Publishers), 265-343
[10] P.F. Castro, T.S.E. Maibaum, A complete and compact propositional deontic logic, in: C.B. Jones, Z. Liu, J. Woodcock (Eds.), ICTAC 2007, LNCS, vol. 4711, 2007, pp. 109-123.; P.F. Castro, T.S.E. Maibaum, A complete and compact propositional deontic logic, in: C.B. Jones, Z. Liu, J. Woodcock (Eds.), ICTAC 2007, LNCS, vol. 4711, 2007, pp. 109-123. · Zbl 1143.03343
[11] Chandra, A. K.; Kozen, D.; Stockmeyer, L. J., Alternation, J. ACM, 28, 1, 114-133 (1981) · Zbl 0473.68043
[12] Chisholm, R. M., Supererogation and offence: a conceptual scheme for ethics, Ratio Juris, 5, 1-14 (1963)
[13] d’Altan, P.; Meyer, J.-J. C.; Wieringa, R., An integrated framework for ought-to-be and ought-to-do constraints, Artif. Intell. Law, 4, 2, 77-111 (1996)
[14] Fenech, S.; Pace, G. J.; Schneider, G., Automatic conflict detection on contracts, (Sixth International Colloquium on Theoretical Aspects of Computing (ICTAC’09). Sixth International Colloquium on Theoretical Aspects of Computing (ICTAC’09), LNCS, vol. 5684 (2009), Springer), 200-214 · Zbl 1250.03049
[15] Fenech, S.; Pace, G. J.; Schneider, G., Clan: a tool for contract analysis and conflict discovery, (Seventh International Symposium on Automated Technology for Verification and Analysis (ATVA’09). Seventh International Symposium on Automated Technology for Verification and Analysis (ATVA’09), LNCS, vol. 5799 (2009), Springer), 90-96
[16] Fischer, M. J.; Ladner, R. E., Propositional modal logic of programs, (Ninth ACM Symposium on Theory of Computing (STOC’77) (1977), ACM), 286-294
[17] E. Grädel, Why are modal logics so robustly decidable? in: Current Trends in Theoretical Computer Science, 2001, pp. 393-408.; E. Grädel, Why are modal logics so robustly decidable? in: Current Trends in Theoretical Computer Science, 2001, pp. 393-408.
[18] Harel, D., Recurring dominoes: making the highly undecidable highly understandable (preliminary report), (Karpinski, M., Fundamentals of Computation Theory (FCT’83). Fundamentals of Computation Theory (FCT’83), LNCS, vol. 158 (1983), Springer), 177-194 · Zbl 0531.68002
[19] Harel, D.; Sherman, R., Propositional dynamic logic of flowcharts, (Karpinski, M., Fundamentals of Computation Theory (FCT’83). Fundamentals of Computation Theory (FCT’83), LNCS, vol. 158 (1983), Springer), 195-206 · Zbl 0534.68021
[20] Harel, D.; Kozen, D.; Tiuryn, J., Dynamic Logic (2000), MIT Press · Zbl 0976.68108
[21] Hoare, C. A.R., Communicating Sequential Processes (1985), Prentice Hall · Zbl 0637.68007
[22] Kozen, D.; Parikh, R., A decision procedure for the propositional \(μ\)-calculus, (Clarke, E. M.; Kozen, D., Fourth Workshop on Logics of Programs. Fourth Workshop on Logics of Programs, LNCS, vol. 164 (1983), Springer), 313-325
[23] Kyas, M.; Prisacariu, C.; Schneider, G., Run-time monitoring of electronic contracts, (ATVA’08. ATVA’08, LNCS, vol. 5311 (2008), Springer), 397-407 · Zbl 1183.68074
[24] Lutz, C.; Walther, D., PDL with negation of atomic programs, (Basin, D. A.; Rusinowitch, M., Second International Joint Conference on Automated Reasoning (IJCAR’04). Second International Joint Conference on Automated Reasoning (IJCAR’04), LNCS, vol. 3097 (2004), Springer), 259-273 · Zbl 1126.03315
[25] McNamara, P., Deontic logic, (Gabbay, D. M.; Woods, J., Handbook of the History of Logic, vol. 7 (2006), North Holland Publishing), 197-289
[26] Meyer, J.-J. C., A different approach to deontic logic: deontic logic viewed as a variant of dynamic logic, Notre Dame J. Formal Logic, 29, 1, 109-136 (1988) · Zbl 0695.03009
[27] J.-J.C. Meyer, F. Dignum, R. Wieringa, The paradoxes of deontic logic revisited: a computer science perspective, Tech. Rep. UU-CS-1994-38, Department of Information and Computing Sciences, Utrecht University, 1994.; J.-J.C. Meyer, F. Dignum, R. Wieringa, The paradoxes of deontic logic revisited: a computer science perspective, Tech. Rep. UU-CS-1994-38, Department of Information and Computing Sciences, Utrecht University, 1994.
[28] Milner, R., Calculi for synchrony and asynchrony, Theoret. Comput. Sci., 25, 267-310 (1983) · Zbl 0512.68026
[29] Milner, R., Communication and Concurrency (1995), Prentice Hall
[30] Pace, G.; Prisacariu, C.; Schneider, G., Model checking contracts – a case study, (Namjoshi, K.; Yoneda, T., Fifth International Symposium on Automated Technology for Verification and Analysis (ATVA’07). Fifth International Symposium on Automated Technology for Verification and Analysis (ATVA’07), LNCS, vol. 4762 (2007), Springer), 82-97 · Zbl 1141.68483
[31] Peleg, D., Concurrent dynamic logic (extended abstract), (Seventh ACM Symposium on Theory of Computing (STOC’85) (1985), ACM), 232-239
[32] Peleg, D., Concurrent dynamic logic, J. ACM, 34, 2, 450-479 (1987) · Zbl 0645.03021
[33] Prakken, H.; Sergot, M., Dyadic deontic logic and contrary-to-duty obligation, (Nute, D., Defeasible Deontic Logic (1997), Kluwer Academic Publishers), 223-262, Available from: <citeseer.ist.psu.edu/article/prakken97dyadic.html> · Zbl 0913.03009
[34] Pratt, V. R., Process logic, (Sixth Symposium on Principles of Programming Languages (POPL’79) (1979), ACM), 93-100
[35] A.N. Prior, Escapism: the logical basis of ethics, in: A.I. Melden (Ed.), Essays in Moral Philosophy, 1958, pp. 135-146.; A.N. Prior, Escapism: the logical basis of ethics, in: A.I. Melden (Ed.), Essays in Moral Philosophy, 1958, pp. 135-146.
[36] C. Prisacariu, A Dynamic Deontic Logic over Synchronous Actions, Ph.D. Thesis, Department of Informatics, University of Oslo, 2010.; C. Prisacariu, A Dynamic Deontic Logic over Synchronous Actions, Ph.D. Thesis, Department of Informatics, University of Oslo, 2010. · Zbl 1287.68139
[37] Prisacariu, C., Synchronous Kleene algebra, J. Logic Algebr. Programming, 79, 7, 608-635 (2010) · Zbl 1204.68123
[38] Prisacariu, C.; Schneider, G., A formal language for electronic contracts, (FMOODS’07. FMOODS’07, LNCS, vol. 4468 (2007), Springer), 174-189 · Zbl 1202.68266
[39] Prisacariu, C.; Schneider, G., CL: an action-based logic for reasoning about contracts, (Workshop on Logic, Language, Informations and Computation (WOLLIC’09). Workshop on Logic, Language, Informations and Computation (WOLLIC’09), LNCS, vol. 5514 (2009), Springer), 335-349 · Zbl 1246.68214
[40] Rabin, M. O., Decidability of second-order theories and automata on infinite trees, Trans. Amer. Math. Soc., 141, 1-35 (1969) · Zbl 0221.02031
[41] Ross, A., Imperatives and logic, Theoria, 7, 53-71 (1941)
[42] Sahlqvist, H., Correspondence and completeness in the first- and second-order semantics for modal logic, (Kanger, S., Proceedings of the Third Scandinavian Logic Symposium (1975), North Holland: North Holland Amsterdam), 110-143
[43] Segerberg, K., A deontic logic of action, Studia Logica, 41, 2, 269-282 (1982) · Zbl 0537.03018
[44] Segerberg, K., Getting started: beginnings in the logic of action, Studia Logica, 51, 3/4, 347-378 (1992) · Zbl 0786.03003
[45] Streett, R. S.; Emerson, E. A., The propositional mu-calculus is elementary, (11th International Colloquium on Automata, Languages and Programming (ICALP’84). 11th International Colloquium on Automata, Languages and Programming (ICALP’84), LNCS, vol. 172 (1984), Springer), 465-472 · Zbl 0556.68005
[46] Trypuz, R.; Kulicki, P., Towards metalogical systematisation of deontic action logics based on Boolean algebra, (Governatori, G.; Sartor, G., Tenth International Conference on Deontic Logic in Computer Science (DEON’10). Tenth International Conference on Deontic Logic in Computer Science (DEON’10), LNCS, vol. 6181 (2010), Springer), 132-147 · Zbl 1250.03041
[47] Van der Meyden, R., Dynamic logic of permission, (Mitchell, J., Fifth Annual IEEE Symposium on Logic in Computer Science (LICS’90) (1990), IEEE Computer Society Press), 72-78 · Zbl 0855.03008
[48] Vardi, M. Y., Why is modal logic so robustly decidable?, (Immerman, N.; Kolaitis, P. G., Descriptive Complexity and Finite Models. Descriptive Complexity and Finite Models, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 31 (1996), American Mathematical Society), 149-184 · Zbl 0881.03012
[49] Von Wright, G. H., An Essay in Deontic Logic and the General Theory of Action (1968), North Holland Publishing Co.: North Holland Publishing Co. Amsterdam · Zbl 0172.29203
[50] Von Wright, G. H., Deontic logic, Mind, 60, 1-15 (1951)
[51] Wyner, A. Z., Sequences, obligations, and the contrary-to-duty paradox, (Goble, L.; Meyer, J.-J. C., Eighth International Workshop on Deontic Logic in Computer Science (DEON’06). Eighth International Workshop on Deontic Logic in Computer Science (DEON’06), LNCS, vol. 4048 (2006), Springer), 255-271 · Zbl 1148.68490
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.