{"id":116,"date":"2012-09-05T09:36:33","date_gmt":"2012-09-05T08:36:33","guid":{"rendered":"http:\/\/sites.google.com\/feeds\/content\/site\/tcsunica\/4818392088042769236"},"modified":"2013-11-22T15:37:24","modified_gmt":"2013-11-22T14:37:24","slug":"seminar-circularity-event-structures-and-contracts","status":"publish","type":"post","link":"https:\/\/dottorati.unica.it\/matematicaeinformatica\/2012\/09\/05\/seminar-circularity-event-structures-and-contracts\/","title":{"rendered":"Seminar: Circularity, event structures, and contracts"},"content":{"rendered":"
Upcoming Seminar<\/span>
<\/span><\/font><\/span><\/div><\/div>

Circularity, event structures, and contracts<\/b>

Sept 11, 12.00
Aula C - Palazzo delle Scienze - Cagliari
<\/span><\/font><\/span><\/div><\/div>

<\/span><\/span><\/font><\/span>
Tiziana Cimoli
<\/span><\/b><\/span><\/font><\/span><\/div><\/div>
Dipartimento di Matematica e Informatica - Universit\u00e0 degli Studi di Cagliari<\/span><\/font>
<\/span><\/div><\/div>

Abstract.<\/b> Contracts\n will play an increasingly important role in the specification and \nimplementation of distributed (cloud) systems. Quoting from [1], \u201cAbsent\n radical improvements in security technology, we expect that users will \nuse contracts and courts, rather than clever security engineering, to \nguard against provider malfeasance\u201d. Contracts describe the promised \nbehavior of a software agent, from the point of view of the actions it \nmay perform, the interactions it may participate into, and its goals. A \nprimary use of contracts if that of postponing actual interaction with \nother agents until an agreement on the mutually promised behaviour has \nbeen found. As in the real world, promises are not always kept by \nsoftware systems, and so contracts may be helpful also after the \nagreement to disciplinate the interaction among agents, and to \nestablish liability in case of violations.<\/span>

At\n a very abstract level, a contract can be seen as sets of events, \ntogether with relations to specify the causal dependencies and the \nconflicts between events. This seems to suggest event structures - one \nof the fundamental causal models for concurrency - as a natural \ncandidate for representing contracts. For instance, one can interpret \nthe enabling b|-a of a stable event structure as the contract clause \n\u201cI will do a after you have done b\u201d.<\/span>

However,\n event structures do not capture a crucial aspect of contracts, i.e. the\n capability of reaching an agreement in the presence of circularity in \nthe declared promises. For instance, one would expect that the contract \nwhere A promises a in change of b, and B promises b in change of a, has \nan agreement. This contrasts with the fact that the event structure with enablings b|-a and a|-b has only \none configuration - the empty set. This is because a|-b actually models \nthe fact that b may only happen after a has been done, and b|-a as the \nfact that a may happen after b - and so neither a nor b can happen. Of \ncourse, A could simply declare to do a, without asking b to be performed\n first - but this would not protect A from a misbehaving B.<\/span>

To\n reconcile causality with circularity, A could relax her contract, i.e. \nshe could do a in change of the promise of B to do b. In this case A can\n safely do the first step, because either B does b, or he will be \nculpable of a contract violation. <\/span>

In\n this talk we present an extension of event structures which allows for \nthis kind of reasoning. The contract a||-b (intuitively, \u201cI will do a if\n you promise to do b\u201d) reaches an agreement with the dual contract \nb||-a, while protecting the participant who offers it. We characterise \nconfigurations of these event structures as provability of formulae in \nthe contract logic PCL, an extension of intuitionistic logic with a \n\u201ccontractual implication\u201d connective.<\/span>

We\n then focus on the problem of determining, in any state of the execution\n of a contract, which events have to be done next. This problem is \ntrivial in classical event structures (one has to do the events whose \ncauses have already been done), while it becomes relevant in the \npresence of circularity: indeed, before performing an event a (whose \ncauses have not already been done) one has to be sure that its causes \nwill be done, eventually in the future. Also in this case we devise a \nlogical characterisation via an encoding in the logic PCL.<\/span>

References<\/b>

[1] \u00a0Michael Armbrust, Armando Fox, Rean Griffith, Anthony D. Joseph, Randy Katz, Andy Konwinski, Gunho Lee, David Patterson, Ariel Rabkin, Ion Stoica, Matei Zaharia. A View of Cloud Computing. Communications of the ACM, Vol. 53 No. 4, Pages 50-58, 2010<\/span><\/span><\/font><\/span><\/div><\/td><\/tr><\/tbody><\/table><\/div>","protected":false},"excerpt":{"rendered":"\n\n\n
\n
\n
\n
\n
Upcoming Seminar<\/span>
<\/span><\/span><\/div>\n<\/div>\n

Circularity, event structures, and contracts<\/b><\/p>\n

Sept 11, 12.00
Aula C – Palazzo delle Scienze – Cagliari
<\/span><\/span><\/div>\n<\/div>\n


<\/span><\/span><\/span><\/p>\n
Tiziana Cimoli
<\/span><\/b><\/span><\/span><\/div>\n<\/div>\n
\n
Dipartimento di Matematica e Informatica – Università degli Studi di Cagliari<\/span>
<\/span><\/div>\n<\/div>\n



Abstract.<\/b> Contracts
\n will play an increasingly important role in the specification and
\nimplementation of distributed (cloud) systems. Quoting from [1], “Absent
\n radical improvements in security technology, we expect that users will
\nuse contracts and courts, rather than clever security engineering, to
\nguard against provider malfeasance”. Contracts describe the promised
\nbehavior of a software agent, from the point of view of the actions it
\nmay perform, the interactions it may participate into, and its goals. A
\nprimary use of contracts if that of postponing actual interaction with
\nother agents until an agreement on the mutually promised behaviour has
\nbeen found. As in the real world, promises are not always kept by
\nsoftware systems, and so contracts may be helpful also after the
\nagreement to disciplinate the interaction among agents, and to
\nestablish liability in case of violations.<\/span><\/p>\n

At
\n a very abstract level, a contract can be seen as sets of events,
\ntogether with relations to specify the causal dependencies and the
\nconflicts between events. This seems to suggest event structures – one
\nof the fundamental causal models for concurrency – as a natural
\ncandidate for representing contracts. For instance, one can interpret
\nthe enabling b|-a of a stable event structure as the contract clause
\n“I will do a after you have done b”.<\/span><\/p>\n

However,
\n event structures do not capture a crucial aspect of contracts, i.e. the
\n capability of reaching an agreement in the presence of circularity in
\nthe declared promises. For instance, one would expect that the contract
\nwhere A promises a in change of b, and B promises b in change of a, has
\nan agreement. This contrasts with the fact that the event structure with enablings b|-a and a|-b has only
\none configuration – the empty set. This is because a|-b actually models
\nthe fact that b may only happen after a has been done, and b|-a as the
\nfact that a may happen after b – and so neither a nor b can happen. Of
\ncourse, A could simply declare to do a, without asking b to be performed
\n first – but this would not protect A from a misbehaving B.<\/span><\/p>\n

To
\n reconcile causality with circularity, A could relax her contract, i.e.
\nshe could do a in change of the promise of B to do b. In this case A can
\n safely do the first step, because either B does b, or he will be
\nculpable of a contract violation. <\/span><\/p>\n

In
\n this talk we present an extension of event structures which allows for
\nthis kind of reasoning. The contract a||-b (intuitively, “I will do a if
\n you promise to do b”) reaches an agreement with the dual contract
\nb||-a, while protecting the participant who offers it. We characterise
\nconfigurations of these event structures as provability of formulae in
\nthe contract logic PCL, an extension of intuitionistic logic with a
\n“contractual implication” connective.<\/span><\/p>\n

We
\n then focus on the problem of determining, in any state of the execution
\n of a contract, which events have to be done next. This problem is
\ntrivial in classical event structures (one has to do the events whose
\ncauses have already been done), while it becomes relevant in the
\npresence of circularity: indeed, before performing an event a (whose
\ncauses have not already been done) one has to be sure that its causes
\nwill be done, eventually in the future. Also in this case we devise a
\nlogical characterisation via an encoding in the logic PCL.<\/span><\/p>\n

References<\/b><\/p>\n

[1]  Michael Armbrust, Armando Fox, Rean Griffith, Anthony D. Joseph, Randy Katz, Andy Konwinski, Gunho Lee, David Patterson, Ariel Rabkin, Ion Stoica, Matei Zaharia. A View of Cloud Computing. Communications of the ACM, Vol. 53 No. 4, Pages 50-58, 2010<\/span><\/span><\/span><\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n","protected":false},"author":1325,"featured_media":0,"comment_status":"closed","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[10,13],"tags":[],"class_list":["post-116","post","type-post","status-publish","format-standard","hentry","category-events","category-httpschemas-google-comsites2008announcement","category-10-id","category-13-id","post-seq-1","post-parity-odd","meta-position-corners","fix"],"_links":{"self":[{"href":"https:\/\/dottorati.unica.it\/matematicaeinformatica\/wp-json\/wp\/v2\/posts\/116","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/dottorati.unica.it\/matematicaeinformatica\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/dottorati.unica.it\/matematicaeinformatica\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/dottorati.unica.it\/matematicaeinformatica\/wp-json\/wp\/v2\/users\/1325"}],"replies":[{"embeddable":true,"href":"https:\/\/dottorati.unica.it\/matematicaeinformatica\/wp-json\/wp\/v2\/comments?post=116"}],"version-history":[{"count":1,"href":"https:\/\/dottorati.unica.it\/matematicaeinformatica\/wp-json\/wp\/v2\/posts\/116\/revisions"}],"predecessor-version":[{"id":137,"href":"https:\/\/dottorati.unica.it\/matematicaeinformatica\/wp-json\/wp\/v2\/posts\/116\/revisions\/137"}],"wp:attachment":[{"href":"https:\/\/dottorati.unica.it\/matematicaeinformatica\/wp-json\/wp\/v2\/media?parent=116"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/dottorati.unica.it\/matematicaeinformatica\/wp-json\/wp\/v2\/categories?post=116"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/dottorati.unica.it\/matematicaeinformatica\/wp-json\/wp\/v2\/tags?post=116"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}