Decisions, Games, & Logic Workshop

[e]

[e]

<style>

/*** LAYOUT ***/
 DIV { border: 0px; }
 #leftHand { 
    width: 100%;
    margin: 0px;
    color: #dfa; 
    background: #a90 url(imgs/stippleG.gif);
    text-align: center;
 }
 #leftHand A { color: #dfa;  font-weight: bold; }
 #links { padding: 4px; background: #339 url(imgs/stippleB.gif); color: #adf; font-size: 13px; font-weight:bold; }
 #links A { padding-left: 5px; padding-right: 5px; }
 #leftHand A { color: white; font: bold; }
 #leftHand A.selected { font-size: 18px; }
 #barOne { background: #ff0 url(imgs/stippleB.gif); height: 5px; }
 #barTwo { background: red url(imgs/stippleW.gif); height: 3px; }
 #barThree { background: #00f url(imgs/stippleG.gif); height: 3px; }
 
 #rightHand {
    width: 620px;
    margin-left: auto; margin-right: auto;
    margin-bottom: 30px;
    text-align: left;
 }

/*** WORKINGS ***/
.editlink { position: absolute; }
.editlink { display: none; }
#rightHand div div .editlink  { display: inline; position: static; float: right; color: white; }
#rightHand div div .editlink A { color: #bbb; }
textarea { font-family: inherit; }

/*** STYLE ***/
 BODY, TD, P, TEXTAREA { font-family: verdana, arial, palatino linotype; font-size: 10pt; padding: 0px; margin: 0px; }
 TD { text-align: center; }
 #rightHand TD { vertical-align: center; text-align: left; }
 BODY {  }
 H2 {  }
 H3 { font-size: 10pt; }
 H4 { font-size: 10pt; background: #270; color: white; margin-left: -30px; margin-right: -30px; padding-left: 10px; padding-right: 10px; }
 A { text-decoration: none; color: #009; }
 A:Hover { text-decoration: underline; }
 #michaelmasReading P, #lentReading P, #summerReading P { margin: 0px; }
 #rightHand LI { margin-bottom: 8px; }
 IMG { border: 0px; }
 #rightHand IMG { border: 1px solid black; }
 P { margin-top: 7px; }
 BLOCKQUOTE { margin-left: 12px; }
 #photos IMG { border: 3px black solid; }

/**** PRINT ****/
@media print {

}

</style>

add breaks

[e]

Third Workshop in
Decisions, Games & Logic '09
15 -17 June 2009, HEC Lausanne

HOME PROGRAMME {DECISION THEORY , GAME THEORY , LOGIC } PvEB SWAP SESSION CONTACT SPONSORS INTERNAL

add breaks

[e]

Jacques Duparc: µ-calculus

Tutorial Abstract

The µ-calculus is the extension of modal logic with least and greatest ﬁxpoint operators. It ﬁrst appeared in an unpublished manuscript in [Bakker, J. Scott, D. [1969] A theory of programs. Unpublished manuscript, IBM, Vienna, 1969.], and the ter- minology was ﬁxed in [Kozen, D. [1983] Results on the Propositional µ-Calculus. Theoretical Computer Science, 27 (1983), 333-354.].

As a modal logic, the semantic of µ-calculus is usually given by Kripke models or equivalently transition systems or colored graphs. Transition systems play a central role in computer science for analyzing systems or processes operationally. Therefore, the modal µ-calculus provides formal framework where we can study the role of ﬁxpoints in transition systems, in other words, the role of ﬁxpoints in operational semantics. Moreover the µ-calculus is intimately related to infinite games, since the evaluation of a formula in a given structure require the usual evaluation game of modal logic to go on forever.

More generally the modal µ-calculus stands as an abstract framework to reason about ﬁxpoints in modal logics. Thus it is a meta formal system for many logics used in computer science. From the point of view of operational semantics, it is the right weakening of second order logics (the fragment of second order monadic logic invariant under bisimulation) with enough expressibility for practical use.

Readings

Julian Bradfield, Colin Stirling: Modal mu-Calculi. In P. Blackburn, J. van Benthem, F. Wolter ed.: Handbook of Modal Logic, Elsevier (2006). Download preliminary version of the paper

Biographical Note

Jacques Duparc is Professor of Formal Logic at the HEC Lausanne.

<h2><img src="http://www.hec.unil.ch/unisciences/photos/uni66421.jpg" align="right" />Jacques Duparc: µ-calculus</h2>

Tutorial Abstract 
 The µ-calculus is the extension of modal logic with least and greatest ﬁxpoint 
operators. It ﬁrst appeared in an unpublished manuscript in [Bakker, J. Scott, D. [1969] A theory of programs. Unpublished manuscript, IBM, Vienna, 1969.], and the ter- 
minology was ﬁxed in [Kozen, D. [1983] Results on the Propositional µ-Calculus. Theoretical Computer Science, 27 (1983), 333-354.].

As a modal logic, the semantic of µ-calculus is usually given by Kripke models or equivalently transition systems or colored graphs. Transition systems play a central role in computer science for analyzing systems or processes operationally. Therefore, the modal µ-calculus provides formal framework where we can study the role of ﬁxpoints in transition systems, in other words, the role of ﬁxpoints in operational semantics. Moreover the µ-calculus is intimately related to infinite games, since the evaluation of a
formula in a given structure require the usual evaluation game of modal logic
to go on forever.

More generally the modal µ-calculus stands as an abstract framework to reason about ﬁxpoints in modal logics. Thus it is a meta formal system for many logics used in computer science. From the point of view of operational semantics, it is the right weakening of second order logics (the fragment of second order monadic logic invariant 
under bisimulation) with enough expressibility for practical use.

Readings
<ul>
<li>Julian Bradfield, Colin Stirling: Modal mu-Calculi. In P. Blackburn, J. van Benthem, F. Wolter ed.: Handbook of Modal Logic, Elsevier (2006). <a href="http://homepages.inf.ed.ac.uk/jcb/Research/MLH-bradstir.pdf">Download preliminary version of the paper</a>
</ul>

Biographical Note 
 <a href="http://www.hec.unil.ch/people/jduparc">Jacques Duparc</a> is Professor of Formal Logic at the HEC Lausanne.

add breaks