ERCIM Working Group MLQA - User contributions [en]

https://wiki.ercim.eu/wg/MLQA/api.php?action=feedcontributions&feedformat=atom&user=Ender ERCIM Working Group MLQA - User contributions [en] 2026-04-04T05:07:00Z User contributions MediaWiki 1.43.6 https://wiki.ercim.eu/wg/MLQA/index.php?title=MLQA_2013&diff=464 MLQA 2013 2013-02-25T13:56:20Z

<p>Ender: </p> <hr /> <div><table width="100%" border="0"><br /> <tr><br /> <td><br /> <h1>Models and Logics for Quantitative Analysis</h1><br /> <b>March 24, 2013</b><br /> <b>Rome, Italy</b><br /> </td><br /> <td>&nbsp;</td><br /> </tr><br /> </table><br /> <br /> <hr><br /> <br /> __TOC__<br /> <br /> <h3 id="overview">Overivew</h3> <br /> The fifth annual meeting of the MLQA working group will take place on Sunday 24 March 2013 as part of the European Joint Conferences on Theory And Practice of Software ([http://www.etaps.org ETAPS]) in Rome, Italy. This year edition will be held in parallel with the Quantitative Aspects of Programming Languages and Systems (QAPL) workshop. Invited speakers will be shared between the two events.<br /> <br /> <br /> <hr><br /> <br /> <h3 id="speakers">Invited speakers</h3> <br /> <br /> <ul><br /> <li>[http://hs.informatik.uni-oldenburg.de/25665.html Martin Fränzle], University of Oldenburg<br><br /> <em>A tight integration of symbolic, numeric, and statistical methods for the analysis of cyber-physical systems</em></li><br /> <li>[https://sites.google.com/site/zupaolo/ Paolo Zuliani], Newcastle University<br><br /> <em>Statistical Model Checking for Cyber-Physical Systems</em></li><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> <em>Guarding against Denial of Service Attacks</em></li><br /> </ul><br /> <br /> <p>Abstracts of the invited talks are available [[#abstractsLONG|here]].</p><br /> <br /> <hr><br /> <br /> <h3 id="programme">Preliminary Programme</h3><br /> <br /> <ul><br /> <li>09:00 - 10:00 Invited talk: <em>A tight integration of symbolic, numeric, and statistical methods for the analysis of cyber-physical systems</em>, by Martin Fränzle<br /> </li><br /> <li>10:00 - 11:00 Invited talk: <em>Statistical Model Checking for Cyber-Physical Systems</em>, by Paolo Zuliani<br /> </li><br /> <li>11:00 - 11:30 <em>coffee</em><br /> </li><br /> <li>11:30 - 12:30 Invited talk: <em>Guarding against Denial of Service Attacks</em>, by Flemming Nielson</li><br /> </ul><br /> <br /> <hr><br /> <br /> <h3 id="organisers">Organiser</h3><br /> <ul><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> </ul><br /> <br /> <hr><br /> <br /> <br /> <div id="minutes"></div><br /> <h3 id="minutess">Minutes</h3><br /> <br /> Minutes of MLQA 2013 will be available after the workshop.<br /> <br /> <br /> <br /> <hr><br /> <br /> <div id="abstractsLONG"></div><h3 id="abstracts">Abstracts of Invited Talks</h3><br /> <br /> <ul><br /> <li>[http://hs.informatik.uni-oldenburg.de/25665.html Martin Fränzle], University of Oldenburg<br><br /> Title: <em>A tight integration of symbolic, numeric, and statistical methods for the analysis of cyber-physical systems</em><br><br /> Abstract: Cyber-physical systems emerge in various application domains, among them<br /> transportation and power networks, provoking a quest for quantitatively<br /> analyzing them with respect to multiple viewpoints, including<br /> functional safety, reliability, and the interaction of the geometric<br /> perspective with the former two. Based on examples from various domains<br /> under different viewpoints, we identify stochastic hybrid systems as a<br /> model able to represent the dynamics relevant to these different<br /> viewpoints. We suggest a symbolic representation of their analysis<br /> problems based on an appropriate hybrid logic and present analysis tools<br /> automatically discharging the proof obligations arising by a blend of<br /> symbolic, safe numeric, and statistical reasoning.<br /> <br /> </li><br /> <li>[https://sites.google.com/site/zupaolo/ Paolo Zuliani], Newcastle University<br><br /> Title: <em>Statistical Model Checking for Cyber-Physical Systems</em><br><br /> Abstract: Statistical model checking is a simulation-based approach for verifying temporal logic properties of complex stochastic systems. Traditional model checking techniques work by searching efficiently the entire state space of the system. However, many interesting systems (e.g., cyber-physical systems) have exceedingly large, or even infinite, state spaces. This makes techniques based on exhaustive search unfeasible. Statistical model checking is instead based on sampling and system simulation, and thereby scales better with system size. We present a statistical model checking approach based on Bayesian statistics, and we apply it to cyber-physical systems coded as Stateflow/Simulink models. Next, we illustrate recent developments involving rare events and non-deterministic systems. We conclude by discussing the strength and weaknesses of the approach and possible directions for future research.<br /> <br><br></li><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> Title: <em>Guarding against Denial of Service Attacks</em><br><br /> Abstract: We outline an approach to the design of systems ensuring that the best possible operation is guaranteed even in the presence of denial of service attacks. As our vehicle of exposition we choose a process calculus allowing to time-out on expected inputs, to base subsequent actions on the extent to which expected inputs were successful and to suitably encrypt the messages exchanged. This is accompanied by an array of analysis techniques for determining the extent to which suitable caution has been exercised: a robustness analysis for ensuring that default data are available when actual data is missing, a safety and security analysis for additionally ensuring that flow of information does not violate integrity models like the Biba model, and a quantitative analysis for determining the probability distributions over the trustworthiness of the data upon which decisions are made.<br /> <br><br></li><br /> </ul></div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=MLQA_2013&diff=463 MLQA 2013 2013-02-24T21:34:41Z

<p>Ender: </p> <hr /> <div><table width="100%" border="0"><br /> <tr><br /> <td><br /> <h1>Models and Logics for Quantitative Analysis</h1><br /> <b>March 24, 2013</b><br /> <b>Rome, Italy</b><br /> </td><br /> <td>&nbsp;</td><br /> </tr><br /> </table><br /> <br /> <hr><br /> <br /> __TOC__<br /> <br /> <h3 id="overview">Overivew</h3> <br /> The fifth annual meeting of the MLQA working group will take place on Sunday 24 March 2013 as part of the European Joint Conferences on Theory And Practice of Software ([http://www.etaps.org ETAPS]) in Rome, Italy. This year edition will be held in parallel with the Quantitative Aspects of Programming Languages and Systems (QAPL) workshop. Invited speakers will be shared between the two events.<br /> <br /> <br /> <hr><br /> <br /> <h3 id="speakers">Invited speakers</h3> <br /> <br /> <ul><br /> <li>[http://hs.informatik.uni-oldenburg.de/25665.html Martin Fränzle], University of Oldenburg<br><br /> <em>A tight integration of symbolic, numeric, and statistical methods for the analysis of cyber-physical systems</em></li><br /> <li>[https://sites.google.com/site/zupaolo/ Paolo Zuliani], Newcastle University<br><br /> <em>Statistical Model Checking for Cyber-Physical Systems</em></li><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> <em>Guarding against Denial of Service Attacks</em></li><br /> </ul><br /> <br /> <p>Abstracts of the invited talks are available [[#abstractsLONG|here]].</p><br /> <br /> <hr><br /> <br /> <h3 id="programme">Preliminary Programme</h3><br /> <br /> <ul><br /> <li>09:00 - 10:00 Invited talk: <em>A tight integration of symbolic, numeric, and statistical methods for the analysis of cyber-physical systems</em>, by Martin Fränzle<br /> </li><br /> <li>10:00 - 11:00 Invited talk: <em>Statistical Model Checking for Cyber-Physical Systems</em>, by Paolo Zuliani<br /> </li><br /> <li>11:00 - 11:30 <em>coffee</em><br /> </li><br /> <li>11:30 - 12:30 Invited talk: <em>Guarding against Denial of Service Attacks</em>, by Flemming Nielson</li><br /> <li>12:30 - 14:00 <em>lunch </em><br /> </li><br /> </ul><br /> <br /> <hr><br /> <br /> <h3 id="organisers">Organiser</h3><br /> <ul><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> </ul><br /> <br /> <hr><br /> <br /> <br /> <div id="minutes"></div><br /> <h3 id="minutess">Minutes</h3><br /> <br /> Minutes of MLQA 2013 will be available after the workshop.<br /> <br /> <br /> <br /> <hr><br /> <br /> <div id="abstractsLONG"></div><h3 id="abstracts">Abstracts of Invited Talks</h3><br /> <br /> <ul><br /> <li>[http://hs.informatik.uni-oldenburg.de/25665.html Martin Fränzle], University of Oldenburg<br><br /> Title: <em>A tight integration of symbolic, numeric, and statistical methods for the analysis of cyber-physical systems</em><br><br /> Abstract: Cyber-physical systems emerge in various application domains, among them<br /> transportation and power networks, provoking a quest for quantitatively<br /> analyzing them with respect to multiple viewpoints, including<br /> functional safety, reliability, and the interaction of the geometric<br /> perspective with the former two. Based on examples from various domains<br /> under different viewpoints, we identify stochastic hybrid systems as a<br /> model able to represent the dynamics relevant to these different<br /> viewpoints. We suggest a symbolic representation of their analysis<br /> problems based on an appropriate hybrid logic and present analysis tools<br /> automatically discharging the proof obligations arising by a blend of<br /> symbolic, safe numeric, and statistical reasoning.<br /> <br /> </li><br /> <li>[https://sites.google.com/site/zupaolo/ Paolo Zuliani], Newcastle University<br><br /> Title: <em>Statistical Model Checking for Cyber-Physical Systems</em><br><br /> Abstract: Statistical model checking is a simulation-based approach for verifying temporal logic properties of complex stochastic systems. Traditional model checking techniques work by searching efficiently the entire state space of the system. However, many interesting systems (e.g., cyber-physical systems) have exceedingly large, or even infinite, state spaces. This makes techniques based on exhaustive search unfeasible. Statistical model checking is instead based on sampling and system simulation, and thereby scales better with system size. We present a statistical model checking approach based on Bayesian statistics, and we apply it to cyber-physical systems coded as Stateflow/Simulink models. Next, we illustrate recent developments involving rare events and non-deterministic systems. We conclude by discussing the strength and weaknesses of the approach and possible directions for future research.<br /> <br><br></li><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> Title: <em>Guarding against Denial of Service Attacks</em><br><br /> Abstract: We outline an approach to the design of systems ensuring that the best possible operation is guaranteed even in the presence of denial of service attacks. As our vehicle of exposition we choose a process calculus allowing to time-out on expected inputs, to base subsequent actions on the extent to which expected inputs were successful and to suitably encrypt the messages exchanged. This is accompanied by an array of analysis techniques for determining the extent to which suitable caution has been exercised: a robustness analysis for ensuring that default data are available when actual data is missing, a safety and security analysis for additionally ensuring that flow of information does not violate integrity models like the Biba model, and a quantitative analysis for determining the probability distributions over the trustworthiness of the data upon which decisions are made.<br /> <br><br></li><br /> </ul></div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=MLQA_2013&diff=462 MLQA 2013 2013-01-18T12:22:42Z

<p>Ender: </p> <hr /> <div><table width="100%" border="0"><br /> <tr><br /> <td><br /> <h1>Models and Logics for Quantitative Analysis</h1><br /> <b>March 24, 2013</b><br /> <b>Rome, Italy</b><br /> </td><br /> <td>&nbsp;</td><br /> </tr><br /> </table><br /> <br /> <hr><br /> <br /> __TOC__<br /> <br /> <h3 id="overview">Overivew</h3> <br /> The fifth annual meeting of the MLQA working group will take place on Sunday 24 March 2013 as part of the European Joint Conferences on Theory And Practice of Software ([http://www.etaps.org ETAPS]) in Rome, Italy. This year edition will be held in parallel with the Quantitative Aspects of Programming Languages and Systems (QAPL) workshop. Invited speakers will be shared between the two events.<br /> <br /> <br /> <hr><br /> <br /> <h3 id="speakers">Invited speakers</h3> <br /> <br /> <ul><br /> <li>[http://hs.informatik.uni-oldenburg.de/25665.html Martin Fränzle], University of Oldenburg<br><br /> <em>A tight integration of symbolic, numeric, and statistical methods for the analysis of cyber-physical systems</em></li><br /> <li>[https://sites.google.com/site/zupaolo/ Paolo Zuliani], Newcastle University<br><br /> <em>Statistical Model Checking for Cyber-Physical Systems</em></li><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> <em>Guarding against Denial of Service Attacks</em></li><br /> </ul><br /> <br /> <p>Abstracts of the invited talks are available [[#abstractsLONG|here]].</p><br /> <br /> <hr><br /> <br /> <h3 id="programme">Preliminary Programme</h3><br /> <br /> <ul><br /> <li>09:00 - 10:00 Invited talk: <em>A tight integration of symbolic, numeric, and statistical methods for the analysis of cyber-physical systems</em>, by Martin Fränzle<br /> </li><br /> <li>10:00 - 11:00 Invited talk: <em>Statistical Model Checking for Cyber-Physical Systems</em>, by Paolo Zuliani<br /> </li><br /> <li>11:00 - 11:30 <em>coffee</em><br /> </li><br /> <li>11:30 - 12:30 Invited talk: <em>Guarding against Denial of Service Attacks</em>, by Flemming Nielson</li><br /> <li>12:30 - 14:00 <em>lunch </em><br /> </li><br /> <li>14:00 - 14:30 <em>MLQA Business Meeting</em><br /> </li><br /> </ul><br /> <br /> <hr><br /> <br /> <h3 id="organisers">Organiser</h3><br /> <ul><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> </ul><br /> <br /> <hr><br /> <br /> <br /> <div id="minutes"></div><br /> <h3 id="minutess">Minutes</h3><br /> <br /> Minutes of MLQA 2013 will be available after the workshop.<br /> <br /> <br /> <br /> <hr><br /> <br /> <div id="abstractsLONG"></div><h3 id="abstracts">Abstracts of Invited Talks</h3><br /> <br /> <ul><br /> <li>[http://hs.informatik.uni-oldenburg.de/25665.html Martin Fränzle], University of Oldenburg<br><br /> Title: <em>A tight integration of symbolic, numeric, and statistical methods for the analysis of cyber-physical systems</em><br><br /> Abstract: Cyber-physical systems emerge in various application domains, among them<br /> transportation and power networks, provoking a quest for quantitatively<br /> analyzing them with respect to multiple viewpoints, including<br /> functional safety, reliability, and the interaction of the geometric<br /> perspective with the former two. Based on examples from various domains<br /> under different viewpoints, we identify stochastic hybrid systems as a<br /> model able to represent the dynamics relevant to these different<br /> viewpoints. We suggest a symbolic representation of their analysis<br /> problems based on an appropriate hybrid logic and present analysis tools<br /> automatically discharging the proof obligations arising by a blend of<br /> symbolic, safe numeric, and statistical reasoning.<br /> <br /> </li><br /> <li>[https://sites.google.com/site/zupaolo/ Paolo Zuliani], Newcastle University<br><br /> Title: <em>Statistical Model Checking for Cyber-Physical Systems</em><br><br /> Abstract: Statistical model checking is a simulation-based approach for verifying temporal logic properties of complex stochastic systems. Traditional model checking techniques work by searching efficiently the entire state space of the system. However, many interesting systems (e.g., cyber-physical systems) have exceedingly large, or even infinite, state spaces. This makes techniques based on exhaustive search unfeasible. Statistical model checking is instead based on sampling and system simulation, and thereby scales better with system size. We present a statistical model checking approach based on Bayesian statistics, and we apply it to cyber-physical systems coded as Stateflow/Simulink models. Next, we illustrate recent developments involving rare events and non-deterministic systems. We conclude by discussing the strength and weaknesses of the approach and possible directions for future research.<br /> <br><br></li><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> Title: <em>Guarding against Denial of Service Attacks</em><br><br /> Abstract: We outline an approach to the design of systems ensuring that the best possible operation is guaranteed even in the presence of denial of service attacks. As our vehicle of exposition we choose a process calculus allowing to time-out on expected inputs, to base subsequent actions on the extent to which expected inputs were successful and to suitably encrypt the messages exchanged. This is accompanied by an array of analysis techniques for determining the extent to which suitable caution has been exercised: a robustness analysis for ensuring that default data are available when actual data is missing, a safety and security analysis for additionally ensuring that flow of information does not violate integrity models like the Biba model, and a quantitative analysis for determining the probability distributions over the trustworthiness of the data upon which decisions are made.<br /> <br><br></li><br /> </ul></div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=MLQA_2013&diff=461 MLQA 2013 2013-01-18T12:22:05Z

<p>Ender: </p> <hr /> <div><table width="100%" border="0"><br /> <tr><br /> <td><br /> <h1>Models and Logics for Quantitative Analysis</h1><br /> <b>March 24, 2013</b><br /> <b>Rome, Italy</b><br /> </td><br /> <td>&nbsp;</td><br /> </tr><br /> </table><br /> <br /> <hr><br /> <br /> __TOC__<br /> <br /> <h3 id="overview">Overivew</h3> <br /> The fifth annual meeting of the MLQA working group will take place on Sunday 24 March 2013 as part of the European Joint Conferences on Theory And Practice of Software ([http://www.etaps.org ETAPS]) in Rome, Italy. This year edition will be held in parallel with the Quantitative Aspects of Programming Languages and Systems (QAPL) workshop. Invited speakers will be shared between the two events.<br /> <br /> <br /> <hr><br /> <br /> <h3 id="speakers">Invited speakers</h3> <br /> <br /> <ul><br /> <li>[http://hs.informatik.uni-oldenburg.de/25665.html Martin Fränzle], University of Oldenburg<br><br /> <em>A tight integration of symbolic, numeric, and statistical methods for the analysis of cyber-physical systems</em></li><br /> <li>[https://sites.google.com/site/zupaolo/ Paolo Zuliani], Newcastle University<br><br /> <em>Statistical Model Checking for Cyber-Physical Systems</em></li><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> <em>Guarding against Denial of Service Attacks</em></li><br /> </ul><br /> <br /> <p>Abstracts of the invited talks are available [[#abstractsLONG|here]].</p><br /> <br /> <hr><br /> <br /> <h3 id="programme">Preliminary Programme</h3><br /> <br /> <ul><br /> <li>09:00 - 10:00 Invited talk: <em>A tight integration of symbolic, numeric, and statistical methods for the analysis of cyber-physical systems</em>, by Martin Fränzle<br /> </li><br /> <li>10:00 - 11:00 Invited talk: <em>Statistical Model Checking for Cyber-Physical Systems</em>, by Paolo Zuliani<br /> <br><br><br /> </li><br /> <li>11:00 - 11:30 <em>coffee</em><br /> <br><br><br /> </li><br /> <li>11:30 - 12:30 Invited talk: <em>Guarding against Denial of Service Attacks</em>, by Flemming Nielson</li><br /> <li>12:30 - 14:00 <em>lunch </em><br /> <br><br><br /> </li><br /> <li>14:00 - 14:30 <em>MLQA Business Meeting</em><br /> </li><br /> </ul><br /> <br /> <hr><br /> <br /> <h3 id="organisers">Organiser</h3><br /> <ul><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> </ul><br /> <br /> <hr><br /> <br /> <br /> <div id="minutes"></div><br /> <h3 id="minutess">Minutes</h3><br /> <br /> Minutes of MLQA 2013 will be available after the workshop.<br /> <br /> <br /> <br /> <hr><br /> <br /> <div id="abstractsLONG"></div><h3 id="abstracts">Abstracts of Invited Talks</h3><br /> <br /> <ul><br /> <li>[http://hs.informatik.uni-oldenburg.de/25665.html Martin Fränzle], University of Oldenburg<br><br /> Title: <em>A tight integration of symbolic, numeric, and statistical methods for the analysis of cyber-physical systems</em><br><br /> Abstract: Cyber-physical systems emerge in various application domains, among them<br /> transportation and power networks, provoking a quest for quantitatively<br /> analyzing them with respect to multiple viewpoints, including<br /> functional safety, reliability, and the interaction of the geometric<br /> perspective with the former two. Based on examples from various domains<br /> under different viewpoints, we identify stochastic hybrid systems as a<br /> model able to represent the dynamics relevant to these different<br /> viewpoints. We suggest a symbolic representation of their analysis<br /> problems based on an appropriate hybrid logic and present analysis tools<br /> automatically discharging the proof obligations arising by a blend of<br /> symbolic, safe numeric, and statistical reasoning.<br /> <br /> </li><br /> <li>[https://sites.google.com/site/zupaolo/ Paolo Zuliani], Newcastle University<br><br /> Title: <em>Statistical Model Checking for Cyber-Physical Systems</em><br><br /> Abstract: Statistical model checking is a simulation-based approach for verifying temporal logic properties of complex stochastic systems. Traditional model checking techniques work by searching efficiently the entire state space of the system. However, many interesting systems (e.g., cyber-physical systems) have exceedingly large, or even infinite, state spaces. This makes techniques based on exhaustive search unfeasible. Statistical model checking is instead based on sampling and system simulation, and thereby scales better with system size. We present a statistical model checking approach based on Bayesian statistics, and we apply it to cyber-physical systems coded as Stateflow/Simulink models. Next, we illustrate recent developments involving rare events and non-deterministic systems. We conclude by discussing the strength and weaknesses of the approach and possible directions for future research.<br /> <br><br></li><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> Title: <em>Guarding against Denial of Service Attacks</em><br><br /> Abstract: We outline an approach to the design of systems ensuring that the best possible operation is guaranteed even in the presence of denial of service attacks. As our vehicle of exposition we choose a process calculus allowing to time-out on expected inputs, to base subsequent actions on the extent to which expected inputs were successful and to suitably encrypt the messages exchanged. This is accompanied by an array of analysis techniques for determining the extent to which suitable caution has been exercised: a robustness analysis for ensuring that default data are available when actual data is missing, a safety and security analysis for additionally ensuring that flow of information does not violate integrity models like the Biba model, and a quantitative analysis for determining the probability distributions over the trustworthiness of the data upon which decisions are made.<br /> <br><br></li><br /> </ul></div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=MLQA_2013&diff=460 MLQA 2013 2013-01-18T12:20:11Z

<p>Ender: </p> <hr /> <div><table width="100%" border="0"><br /> <tr><br /> <td><br /> <h1>Models and Logics for Quantitative Analysis</h1><br /> <b>March 24, 2013</b><br /> <b>Rome, Italy</b><br /> </td><br /> <td>&nbsp;</td><br /> </tr><br /> </table><br /> <br /> <hr><br /> <br /> __TOC__<br /> <br /> <h3 id="overview">Overivew</h3> <br /> The fifth annual meeting of the MLQA working group will take place on Sunday 24 March 2013 as part of the European Joint Conferences on Theory And Practice of Software ([http://www.etaps.org ETAPS]) in Rome, Italy. This year edition will be held in parallel with the Quantitative Aspects of Programming Languages and Systems (QAPL) workshop. Invited speakers will be shared between the two events.<br /> <br /> <br /> <hr><br /> <br /> <h3 id="speakers">Invited speakers</h3> <br /> <br /> <ul><br /> <li>[http://hs.informatik.uni-oldenburg.de/25665.html Martin Fränzle], University of Oldenburg<br><br /> <em>A tight integration of symbolic, numeric, and statistical methods for the analysis of cyber-physical systems</em></li><br /> <li>[https://sites.google.com/site/zupaolo/ Paolo Zuliani], Newcastle University<br><br /> <em>Statistical Model Checking for Cyber-Physical Systems</em></li><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> <em>Guarding against Denial of Service Attacks</em></li><br /> </ul><br /> <br /> <p>Abstracts of the invited talks are available [[#abstractsLONG|here]].</p><br /> <br /> <hr><br /> <br /> <h3 id="programme">Preliminary Programme</h3><br /> <br /> <ul><br /> <li>09:00 - 10:00 <em>Opening</em><br /> </li><br /> <li>10:00 - 11:00 invited talk: <em>Statistical Model Checking for Cyber-Physical Systems</em>, by Paolo Zuliani<br /> <br><br><br /> </li><br /> <li>11:00 - 11:30 <em>coffee</em><br /> <br><br><br /> </li><br /> <li>11:30 - 12:30 <em>Invited talk</em></li><br /> <li>12:30 - 14:00 <em>lunch </em><br /> <br><br><br /> </li><br /> <li>14:00 - 14:30 <em>MLQA Business Meeting</em><br /> </li><br /> </ul><br /> <br /> <hr><br /> <br /> <h3 id="organisers">Organiser</h3><br /> <ul><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> </ul><br /> <br /> <hr><br /> <br /> <br /> <div id="minutes"></div><br /> <h3 id="minutess">Minutes</h3><br /> <br /> Minutes of MLQA 2013 will be available after the workshop.<br /> <br /> <br /> <br /> <hr><br /> <br /> <div id="abstractsLONG"></div><h3 id="abstracts">Abstracts of Invited Talks</h3><br /> <br /> <ul><br /> <li>[http://hs.informatik.uni-oldenburg.de/25665.html Martin Fränzle], University of Oldenburg<br><br /> Title: <em>A tight integration of symbolic, numeric, and statistical methods for the analysis of cyber-physical systems</em><br><br /> Abstract: Cyber-physical systems emerge in various application domains, among them<br /> transportation and power networks, provoking a quest for quantitatively<br /> analyzing them with respect to multiple viewpoints, including<br /> functional safety, reliability, and the interaction of the geometric<br /> perspective with the former two. Based on examples from various domains<br /> under different viewpoints, we identify stochastic hybrid systems as a<br /> model able to represent the dynamics relevant to these different<br /> viewpoints. We suggest a symbolic representation of their analysis<br /> problems based on an appropriate hybrid logic and present analysis tools<br /> automatically discharging the proof obligations arising by a blend of<br /> symbolic, safe numeric, and statistical reasoning.<br /> <br /> </li><br /> <li>[https://sites.google.com/site/zupaolo/ Paolo Zuliani], Newcastle University<br><br /> Title: <em>Statistical Model Checking for Cyber-Physical Systems</em><br><br /> Abstract: Statistical model checking is a simulation-based approach for verifying temporal logic properties of complex stochastic systems. Traditional model checking techniques work by searching efficiently the entire state space of the system. However, many interesting systems (e.g., cyber-physical systems) have exceedingly large, or even infinite, state spaces. This makes techniques based on exhaustive search unfeasible. Statistical model checking is instead based on sampling and system simulation, and thereby scales better with system size. We present a statistical model checking approach based on Bayesian statistics, and we apply it to cyber-physical systems coded as Stateflow/Simulink models. Next, we illustrate recent developments involving rare events and non-deterministic systems. We conclude by discussing the strength and weaknesses of the approach and possible directions for future research.<br /> <br><br></li><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> Title: <em>Guarding against Denial of Service Attacks</em><br><br /> Abstract: We outline an approach to the design of systems ensuring that the best possible operation is guaranteed even in the presence of denial of service attacks. As our vehicle of exposition we choose a process calculus allowing to time-out on expected inputs, to base subsequent actions on the extent to which expected inputs were successful and to suitably encrypt the messages exchanged. This is accompanied by an array of analysis techniques for determining the extent to which suitable caution has been exercised: a robustness analysis for ensuring that default data are available when actual data is missing, a safety and security analysis for additionally ensuring that flow of information does not violate integrity models like the Biba model, and a quantitative analysis for determining the probability distributions over the trustworthiness of the data upon which decisions are made.<br /> <br><br></li><br /> </ul></div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=MLQA_2013&diff=459 MLQA 2013 2013-01-18T12:18:49Z

<p>Ender: </p> <hr /> <div><table width="100%" border="0"><br /> <tr><br /> <td><br /> <h1>Models and Logics for Quantitative Analysis</h1><br /> <b>March 24, 2013</b><br /> <b>Rome, Italy</b><br /> </td><br /> <td>&nbsp;</td><br /> </tr><br /> </table><br /> <br /> <hr><br /> <br /> __TOC__<br /> <br /> <h3 id="overview">Overivew</h3> <br /> The fifth annual meeting of the MLQA working group will take place on Sunday 24 March 2013 as part of the European Joint Conferences on Theory And Practice of Software ([http://www.etaps.org ETAPS]) in Rome, Italy. This year edition will be held in parallel with the Quantitative Aspects of Programming Languages and Systems (QAPL) workshop. Invited speakers will be shared between the two events.<br /> <br /> <br /> <hr><br /> <br /> <h3 id="speakers">Invited speakers</h3> <br /> <br /> <ul><br /> <li>[http://hs.informatik.uni-oldenburg.de/25665.html Martin Fränzle], University of Oldenburg<br><br /> <em>A tight integration of symbolic, numeric, and statistical methods for the analysis of cyber-physical systems</em></li><br /> <li>[https://sites.google.com/site/zupaolo/ Paolo Zuliani], Newcastle University<br><br /> <em>Statistical Model Checking for Cyber-Physical Systems</em></li><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> <em>Guarding against Denial of Service Attacks</em></li><br /> </ul><br /> <br /> <p>Abstracts of the invited talks are available [[#abstractsLONG|here]].</p><br /> <br /> <hr><br /> <br /> <h3 id="programme">Preliminary Programme</h3><br /> <br /> <ul><br /> <li>09:00 - 10:00 <em>Opening</em><br /> </li><br /> <li>10:00 - 11:00 <em>invited talk</em><br /> <br><br><br /> </li><br /> <li>11:00 - 11:30 <em>coffee</em><br /> <br><br><br /> </li><br /> <li>11:30 - 12:30 <em>Invited talk</em></li><br /> <li>12:30 - 14:00 <em>lunch </em><br /> <br><br><br /> </li><br /> <li>14:00 - 14:30 <em>MLQA Business Meeting</em><br /> </li><br /> </ul><br /> <br /> <hr><br /> <br /> <h3 id="organisers">Organiser</h3><br /> <ul><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> </ul><br /> <br /> <hr><br /> <br /> <br /> <div id="minutes"></div><br /> <h3 id="minutess">Minutes</h3><br /> <br /> Minutes of MLQA 2013 will be available after the workshop.<br /> <br /> <br /> <br /> <hr><br /> <br /> <div id="abstractsLONG"></div><h3 id="abstracts">Abstracts of Invited Talks</h3><br /> <br /> <ul><br /> <li>[http://hs.informatik.uni-oldenburg.de/25665.html Martin Fränzle], University of Oldenburg<br><br /> Title: <em>A tight integration of symbolic, numeric, and statistical methods for the analysis of cyber-physical systems</em><br><br /> Abstract: Cyber-physical systems emerge in various application domains, among them<br /> transportation and power networks, provoking a quest for quantitatively<br /> analyzing them with respect to multiple viewpoints, including<br /> functional safety, reliability, and the interaction of the geometric<br /> perspective with the former two. Based on examples from various domains<br /> under different viewpoints, we identify stochastic hybrid systems as a<br /> model able to represent the dynamics relevant to these different<br /> viewpoints. We suggest a symbolic representation of their analysis<br /> problems based on an appropriate hybrid logic and present analysis tools<br /> automatically discharging the proof obligations arising by a blend of<br /> symbolic, safe numeric, and statistical reasoning.<br /> <br /> </li><br /> <li>[https://sites.google.com/site/zupaolo/ Paolo Zuliani], Newcastle University<br><br /> Title: <em>Statistical Model Checking for Cyber-Physical Systems</em><br><br /> Abstract: Statistical model checking is a simulation-based approach for verifying temporal logic properties of complex stochastic systems. Traditional model checking techniques work by searching efficiently the entire state space of the system. However, many interesting systems (e.g., cyber-physical systems) have exceedingly large, or even infinite, state spaces. This makes techniques based on exhaustive search unfeasible. Statistical model checking is instead based on sampling and system simulation, and thereby scales better with system size. We present a statistical model checking approach based on Bayesian statistics, and we apply it to cyber-physical systems coded as Stateflow/Simulink models. Next, we illustrate recent developments involving rare events and non-deterministic systems. We conclude by discussing the strength and weaknesses of the approach and possible directions for future research.<br /> <br><br></li><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> Title: <em>Guarding against Denial of Service Attacks</em><br><br /> Abstract: We outline an approach to the design of systems ensuring that the best possible operation is guaranteed even in the presence of denial of service attacks. As our vehicle of exposition we choose a process calculus allowing to time-out on expected inputs, to base subsequent actions on the extent to which expected inputs were successful and to suitably encrypt the messages exchanged. This is accompanied by an array of analysis techniques for determining the extent to which suitable caution has been exercised: a robustness analysis for ensuring that default data are available when actual data is missing, a safety and security analysis for additionally ensuring that flow of information does not violate integrity models like the Biba model, and a quantitative analysis for determining the probability distributions over the trustworthiness of the data upon which decisions are made.<br /> <br><br></li><br /> </ul></div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=MLQA_2013&diff=458 MLQA 2013 2012-11-30T13:48:15Z

<p>Ender: </p> <hr /> <div><table width="100%" border="0"><br /> <tr><br /> <td><br /> <h1>Models and Logics for Quantitative Analysis</h1><br /> <b>March 24, 2013</b><br /> <b>Rome, Italy</b><br /> </td><br /> <td>&nbsp;</td><br /> </tr><br /> </table><br /> <br /> <hr><br /> <br /> __TOC__<br /> <br /> <h3 id="overview">Overivew</h3> <br /> The fifth annual meeting of the MLQA working group will take place on Sunday 24 March 2013 as part of the European Joint Conferences on Theory And Practice of Software ([http://www.etaps.org ETAPS]) in Rome, Italy. This year edition will be held in parallel with the Quantitative Aspects of Programming Languages and Systems (QAPL) workshop. Invited speakers will be shared between the two events.<br /> <br /> <br /> <hr><br /> <br /> <h3 id="speakers">Invited speakers</h3> <br /> <br /> <ul><br /> <li>[http://hs.informatik.uni-oldenburg.de/25665.html Martin Fränzle], University of Oldenburg<br><br /> <em>A tight integration of symbolic, numeric, and statistical methods for the analysis of cyber-physical systems</em></li><br /> <li>[https://sites.google.com/site/zupaolo/ Paolo Zuliani], Newcastle University<br><br /> <em>Statistical Model Checking for Cyber-Physical Systems</em></li><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> <em>Guarding against Denial of Service Attacks</em></li><br /> </ul><br /> <br /> <p>Abstracts of the invited talks are available [[#abstractsLONG|here]].</p><br /> <br /> <hr><br /> <br /> <h3 id="programme">Preliminary Programme</h3><br /> <br /> TBA<br /> <br /> <hr><br /> <br /> <h3 id="organisers">Organiser</h3><br /> <ul><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> </ul><br /> <br /> <hr><br /> <br /> <br /> <div id="minutes"></div><br /> <h3 id="minutess">Minutes</h3><br /> <br /> Minutes of MLQA 2013 will be available after the workshop.<br /> <br /> <br /> <br /> <hr><br /> <br /> <div id="abstractsLONG"></div><h3 id="abstracts">Abstracts of Invited Talks</h3><br /> <br /> <ul><br /> <li>[http://hs.informatik.uni-oldenburg.de/25665.html Martin Fränzle], University of Oldenburg<br><br /> Title: <em>A tight integration of symbolic, numeric, and statistical methods for the analysis of cyber-physical systems</em><br><br /> Abstract: Cyber-physical systems emerge in various application domains, among them<br /> transportation and power networks, provoking a quest for quantitatively<br /> analyzing them with respect to multiple viewpoints, including<br /> functional safety, reliability, and the interaction of the geometric<br /> perspective with the former two. Based on examples from various domains<br /> under different viewpoints, we identify stochastic hybrid systems as a<br /> model able to represent the dynamics relevant to these different<br /> viewpoints. We suggest a symbolic representation of their analysis<br /> problems based on an appropriate hybrid logic and present analysis tools<br /> automatically discharging the proof obligations arising by a blend of<br /> symbolic, safe numeric, and statistical reasoning.<br /> <br /> </li><br /> <li>[https://sites.google.com/site/zupaolo/ Paolo Zuliani], Newcastle University<br><br /> Title: <em>Statistical Model Checking for Cyber-Physical Systems</em><br><br /> Abstract: Statistical model checking is a simulation-based approach for verifying temporal logic properties of complex stochastic systems. Traditional model checking techniques work by searching efficiently the entire state space of the system. However, many interesting systems (e.g., cyber-physical systems) have exceedingly large, or even infinite, state spaces. This makes techniques based on exhaustive search unfeasible. Statistical model checking is instead based on sampling and system simulation, and thereby scales better with system size. We present a statistical model checking approach based on Bayesian statistics, and we apply it to cyber-physical systems coded as Stateflow/Simulink models. Next, we illustrate recent developments involving rare events and non-deterministic systems. We conclude by discussing the strength and weaknesses of the approach and possible directions for future research.<br /> <br><br></li><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> Title: <em>Guarding against Denial of Service Attacks</em><br><br /> Abstract: We outline an approach to the design of systems ensuring that the best possible operation is guaranteed even in the presence of denial of service attacks. As our vehicle of exposition we choose a process calculus allowing to time-out on expected inputs, to base subsequent actions on the extent to which expected inputs were successful and to suitably encrypt the messages exchanged. This is accompanied by an array of analysis techniques for determining the extent to which suitable caution has been exercised: a robustness analysis for ensuring that default data are available when actual data is missing, a safety and security analysis for additionally ensuring that flow of information does not violate integrity models like the Biba model, and a quantitative analysis for determining the probability distributions over the trustworthiness of the data upon which decisions are made.<br /> <br><br></li><br /> </ul></div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=MLQA_2013&diff=457 MLQA 2013 2012-11-29T10:35:35Z

<p>Ender: </p> <hr /> <div><table width="100%" border="0"><br /> <tr><br /> <td><br /> <h1>Models and Logics for Quantitative Analysis</h1><br /> <b>March 24, 2013</b><br /> <b>Rome, Italy</b><br /> </td><br /> <td>&nbsp;</td><br /> </tr><br /> </table><br /> <br /> <hr><br /> <br /> __TOC__<br /> <br /> <h3 id="overivew">Overivew</h3> <br /> The fifth annual meeting of the MLQA working group will take place on Sunday 24 March 2013 as part of the European Joint Conferences on Theory And Practice of Software (ETAPS) in Rome, Italy. This year edition will be held in parallel with the Quantitative Aspects of Programming Languages and Systems (QAPL) workshop. Invited speakers will be shared between the two events.<br /> <br /> <br /> <hr><br /> <br /> <h3 id="speakers">Invited speakers</h3> <br /> <br /> <ul><br /> <li>[http://hs.informatik.uni-oldenburg.de/25665.html Martin Fränzle], University of Oldenburg<br><br /> <em>A tight integration of symbolic, numeric, and statistical methods for the analysis of cyber-physical systems</em></li><br /> <li>[https://sites.google.com/site/zupaolo/ Paolo Zuliani], Newcastle University<br><br /> <em>Statistical Model Checking for Cyber-Physical Systems</em></li><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> <em>Guarding against Denial of Service Attacks</em></li><br /> </ul><br /> <br /> <p>Abstracts of the invited talks are available [[#abstractsLONG|here]].</p><br /> <br /> <hr><br /> <br /> <h3 id="programme">Preliminary Programme</h3><br /> <br /> TBA<br /> <br /> <hr><br /> <br /> <h3 id="organisers">Organiser</h3><br /> <ul><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> </ul><br /> <br /> <hr><br /> <br /> <br /> <div id="minutes"></div><br /> <h3 id="minutess">Minutes</h3><br /> <br /> Minutes of MLQA 2013 will be available after the workshop.<br /> <br /> <br /> <br /> <hr><br /> <br /> <div id="abstractsLONG"></div><h3 id="abstracts">Abstracts of Invited Talks</h3><br /> <br /> <ul><br /> <li>[http://hs.informatik.uni-oldenburg.de/25665.html Martin Fränzle], University of Oldenburg<br><br /> Title: <em>A tight integration of symbolic, numeric, and statistical methods for the analysis of cyber-physical systems</em><br><br /> Abstract: Cyber-physical systems emerge in various application domains, among them<br /> transportation and power networks, provoking a quest for quantitatively<br /> analyzing them with respect to multiple viewpoints, including<br /> functional safety, reliability, and the interaction of the geometric<br /> perspective with the former two. Based on examples from various domains<br /> under different viewpoints, we identify stochastic hybrid systems as a<br /> model able to represent the dynamics relevant to these different<br /> viewpoints. We suggest a symbolic representation of their analysis<br /> problems based on an appropriate hybrid logic and present analysis tools<br /> automatically discharging the proof obligations arising by a blend of<br /> symbolic, safe numeric, and statistical reasoning.<br /> <br /> </li><br /> <li>[https://sites.google.com/site/zupaolo/ Paolo Zuliani], Newcastle University<br><br /> Title: <em>Statistical Model Checking for Cyber-Physical Systems</em><br><br /> Abstract: Statistical model checking is a simulation-based approach for verifying temporal logic properties of complex stochastic systems. Traditional model checking techniques work by searching efficiently the entire state space of the system. However, many interesting systems (e.g., cyber-physical systems) have exceedingly large, or even infinite, state spaces. This makes techniques based on exhaustive search unfeasible. Statistical model checking is instead based on sampling and system simulation, and thereby scales better with system size. We present a statistical model checking approach based on Bayesian statistics, and we apply it to cyber-physical systems coded as Stateflow/Simulink models. Next, we illustrate recent developments involving rare events and non-deterministic systems. We conclude by discussing the strength and weaknesses of the approach and possible directions for future research.<br /> <br><br></li><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> Title: <em>Guarding against Denial of Service Attacks</em><br><br /> Abstract: We outline an approach to the design of systems ensuring that the best possible operation is guaranteed even in the presence of denial of service attacks. As our vehicle of exposition we choose a process calculus allowing to time-out on expected inputs, to base subsequent actions on the extent to which expected inputs were successful and to suitably encrypt the messages exchanged. This is accompanied by an array of analysis techniques for determining the extent to which suitable caution has been exercised: a robustness analysis for ensuring that default data are available when actual data is missing, a safety and security analysis for additionally ensuring that flow of information does not violate integrity models like the Biba model, and a quantitative analysis for determining the probability distributions over the trustworthiness of the data upon which decisions are made.<br /> <br><br></li><br /> </ul></div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=MLQA_2013&diff=456 MLQA 2013 2012-11-27T08:25:45Z

<p>Ender: </p> <hr /> <div><table width="100%" border="0"><br /> <tr><br /> <td><br /> <h1>Models and Logics for Quantitative Analysis</h1><br /> <b>March 24, 2013</b><br /> <b>Rome, Italy</b><br /> </td><br /> <td>&nbsp;</td><br /> </tr><br /> </table><br /> <br /> <hr><br /> <br /> __TOC__<br /> <br /> <h3 id="overivew">Overivew</h3> <br /> The fifth annual meeting of the MLQA working group will take place on Sunday 24 March 2013 as part of the European Joint Conferences on Theory And Practice of Software (ETAPS) in Rome, Italy. This year edition will be held in parallel with the Quantitative Aspects of Programming Languages and Systems (QAPL) workshop. Invited speakers will be shared between the two events.<br /> <br /> <hr><br /> <br /> <h3 id="previous">Past Events</h3> <br /> <br /> [[MLQA 2009|MLQA 2009]], York, UK.<br /> <br /> [[MLQA 2010|MLQA 2010]], Edinburgh, UK.<br /> <br /> [[MLQA 2011|MLQA 2011]], Aachen, Germany.<br /> <br /> [[MLQA 2012]], Edinburgh, UK.<br /> <br /> <br /> <hr><br /> <br /> <h3 id="speakers">Invited speakers</h3> <br /> <br /> <ul><br /> <li>[http://hs.informatik.uni-oldenburg.de/25665.html Martin Fränzle], University of Oldenburg<br><br /> <em>A tight integration of symbolic, numeric, and statistical methods for the analysis of cyber-physical systems</em></li><br /> <li>[https://sites.google.com/site/zupaolo/ Paolo Zuliani], Newcastle University<br><br /> <em>Statistical Model Checking for Cyber-Physical Systems</em></li><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> <em>Guarding against Denial of Service Attacks</em></li><br /> </ul><br /> <br /> <p>Abstracts of the invited talks are available [[#abstractsLONG|here]].</p><br /> <br /> <hr><br /> <br /> <h3 id="programme">Preliminary Programme</h3><br /> <br /> TBA<br /> <br /> <hr><br /> <br /> <h3 id="organisers">Organiser</h3><br /> <ul><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> </ul><br /> <br /> <hr><br /> <br /> <br /> <div id="minutes"></div><br /> <h3 id="minutess">Minutes</h3><br /> <br /> Minutes of MLQA 2013 will be available after the workshop.<br /> <br /> <br /> <br /> <hr><br /> <br /> <div id="abstractsLONG"></div><h3 id="abstracts">Abstracts of Invited Talks</h3><br /> <br /> <ul><br /> <li>[http://hs.informatik.uni-oldenburg.de/25665.html Martin Fränzle], University of Oldenburg<br><br /> Title: <em>A tight integration of symbolic, numeric, and statistical methods for the analysis of cyber-physical systems</em><br><br /> Abstract: Cyber-physical systems emerge in various application domains, among them<br /> transportation and power networks, provoking a quest for quantitatively<br /> analyzing them with respect to multiple viewpoints, including<br /> functional safety, reliability, and the interaction of the geometric<br /> perspective with the former two. Based on examples from various domains<br /> under different viewpoints, we identify stochastic hybrid systems as a<br /> model able to represent the dynamics relevant to these different<br /> viewpoints. We suggest a symbolic representation of their analysis<br /> problems based on an appropriate hybrid logic and present analysis tools<br /> automatically discharging the proof obligations arising by a blend of<br /> symbolic, safe numeric, and statistical reasoning.<br /> <br /> </li><br /> <li>[https://sites.google.com/site/zupaolo/ Paolo Zuliani], Newcastle University<br><br /> Title: <em>Statistical Model Checking for Cyber-Physical Systems</em><br><br /> Abstract: Statistical model checking is a simulation-based approach for verifying temporal logic properties of complex stochastic systems. Traditional model checking techniques work by searching efficiently the entire state space of the system. However, many interesting systems (e.g., cyber-physical systems) have exceedingly large, or even infinite, state spaces. This makes techniques based on exhaustive search unfeasible. Statistical model checking is instead based on sampling and system simulation, and thereby scales better with system size. We present a statistical model checking approach based on Bayesian statistics, and we apply it to cyber-physical systems coded as Stateflow/Simulink models. Next, we illustrate recent developments involving rare events and non-deterministic systems. We conclude by discussing the strength and weaknesses of the approach and possible directions for future research.<br /> <br><br></li><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> Title: <em>Guarding against Denial of Service Attacks</em><br><br /> Abstract: We outline an approach to the design of systems ensuring that the best possible operation is guaranteed even in the presence of denial of service attacks. As our vehicle of exposition we choose a process calculus allowing to time-out on expected inputs, to base subsequent actions on the extent to which expected inputs were successful and to suitably encrypt the messages exchanged. This is accompanied by an array of analysis techniques for determining the extent to which suitable caution has been exercised: a robustness analysis for ensuring that default data are available when actual data is missing, a safety and security analysis for additionally ensuring that flow of information does not violate integrity models like the Biba model, and a quantitative analysis for determining the probability distributions over the trustworthiness of the data upon which decisions are made.<br /> <br><br></li><br /> </ul></div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=MLQA_2013&diff=455 MLQA 2013 2012-11-27T08:23:25Z

<p>Ender: </p> <hr /> <div><table width="100%" border="0"><br /> <tr><br /> <td><br /> <h1>Models and Logics for Quantitative Analysis</h1><br /> <b>March 24, 2013</b><br /> <b>Rome, Italy</b><br /> </td><br /> <td>&nbsp;</td><br /> </tr><br /> </table><br /> <br /> <hr><br /> <br /> __TOC__<br /> <br /> <h3 id="overivew">Overivew</h3> <br /> The fifth annual meeting of the MLQA working group will take place on Sunday 24 March 2013 as part of the European Joint Conferences on Theory And Practice of Software (ETAPS) in Rome, Italy. This year edition will be held in parallel with the Quantitative Aspects of Programming Languages and Systems (QAPL) workshop. Invited speakers will be shared between the two events.<br /> <br /> <hr><br /> <br /> <h3 id="previous">Past Events</h3> <br /> <br /> [[MLQA 2009|MLQA 2009]], York, UK.<br /> <br /> [[MLQA 2010|MLQA 2010]], Edinburgh, UK.<br /> <br /> [[MLQA 2011|MLQA 2011]], Aachen, Germany.<br /> <br /> [[MLQA 2012]], Edinburgh, UK.<br /> <br /> <br /> <hr><br /> <br /> <h3 id="speakers">Invited speakers</h3> <br /> <br /> <ul><br /> <li>[http://hs.informatik.uni-oldenburg.de/25665.html Martin Fränzle], University of Oldenburg<br><br /> <em>A tight integration of symbolic, numeric, and statistical methods for the analysis of cyber-physical systems</em></li><br /> <li>[https://sites.google.com/site/zupaolo/ Paolo Zuliani], Newcastle University<br><br /> <em>Statistical Model Checking for Cyber-Physical Systems</em></li><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> <em>Guarding against Denial of Service Attacks</em></li><br /> </ul><br /> <br /> <p>Abstracts of the invited talks are available [[#abstractsLONG|here]].</p><br /> <br /> <br /> <hr><br /> <br /> <h3 id="registration">Registration</h3><br /> <br /> TBA<br /> <br /> <hr><br /> <br /> <h3 id="programme">Preliminary Programme</h3><br /> <br /> TBA<br /> <br /> <hr><br /> <br /> <h3 id="travel">Travel and Accommodation</h3><br /> <br /> <p><br /> TBA<br /> <hr><br /> <br /> <h3 id="organisers">Organiser</h3><br /> <ul><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> </ul><br /> <br /> <hr><br /> <br /> <br /> <div id="minutes"></div><br /> <h3 id="minutess">Minutes</h3><br /> <br /> Minutes of MLQA 2013 will be available after the workshop.<br /> <br /> <br /> <br /> <hr><br /> <br /> <div id="abstractsLONG"></div><h3 id="abstracts">Abstracts of Invited Talks</h3><br /> <br /> <ul><br /> <li>[http://hs.informatik.uni-oldenburg.de/25665.html Martin Fränzle], University of Oldenburg<br><br /> Title: <em>A tight integration of symbolic, numeric, and statistical methods for the analysis of cyber-physical systems</em><br><br /> Abstract: Cyber-physical systems emerge in various application domains, among them<br /> transportation and power networks, provoking a quest for quantitatively<br /> analyzing them with respect to multiple viewpoints, including<br /> functional safety, reliability, and the interaction of the geometric<br /> perspective with the former two. Based on examples from various domains<br /> under different viewpoints, we identify stochastic hybrid systems as a<br /> model able to represent the dynamics relevant to these different<br /> viewpoints. We suggest a symbolic representation of their analysis<br /> problems based on an appropriate hybrid logic and present analysis tools<br /> automatically discharging the proof obligations arising by a blend of<br /> symbolic, safe numeric, and statistical reasoning.<br /> <br /> </li><br /> <li>[https://sites.google.com/site/zupaolo/ Paolo Zuliani], Newcastle University<br><br /> Title: <em>Statistical Model Checking for Cyber-Physical Systems</em><br><br /> Abstract: Statistical model checking is a simulation-based approach for verifying temporal logic properties of complex stochastic systems. Traditional model checking techniques work by searching efficiently the entire state space of the system. However, many interesting systems (e.g., cyber-physical systems) have exceedingly large, or even infinite, state spaces. This makes techniques based on exhaustive search unfeasible. Statistical model checking is instead based on sampling and system simulation, and thereby scales better with system size. We present a statistical model checking approach based on Bayesian statistics, and we apply it to cyber-physical systems coded as Stateflow/Simulink models. Next, we illustrate recent developments involving rare events and non-deterministic systems. We conclude by discussing the strength and weaknesses of the approach and possible directions for future research.<br /> <br><br></li><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> Title: <em>Guarding against Denial of Service Attacks</em><br><br /> Abstract: We outline an approach to the design of systems ensuring that the best possible operation is guaranteed even in the presence of denial of service attacks. As our vehicle of exposition we choose a process calculus allowing to time-out on expected inputs, to base subsequent actions on the extent to which expected inputs were successful and to suitably encrypt the messages exchanged. This is accompanied by an array of analysis techniques for determining the extent to which suitable caution has been exercised: a robustness analysis for ensuring that default data are available when actual data is missing, a safety and security analysis for additionally ensuring that flow of information does not violate integrity models like the Biba model, and a quantitative analysis for determining the probability distributions over the trustworthiness of the data upon which decisions are made.<br /> <br><br></li><br /> </ul></div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=MLQA_2013&diff=454 MLQA 2013 2012-11-27T08:22:46Z

<p>Ender: </p> <hr /> <div><table width="100%" border="0"><br /> <tr><br /> <td><br /> <h1>Models and Logics for Quantitative Analysis</h1><br /> <b>March 24, 2013</b><br /> <b>Rome, Italy</b><br /> </td><br /> <td>&nbsp;</td><br /> </tr><br /> </table><br /> <br /> <hr><br /> <br /> <h3 id="overivew">Overivew</h3> <br /> The fifth annual meeting of the MLQA working group will take place on Sunday 24 March 2013 as part of the European Joint Conferences on Theory And Practice of Software (ETAPS) in Rome, Italy. This year edition will be held in parallel with the Quantitative Aspects of Programming Languages and Systems (QAPL) workshop. Invited speakers will be shared between the two events.<br /> <br /> <hr><br /> <br /> <h3 id="previous">Past Events</h3> <br /> <br /> [[MLQA 2009|MLQA 2009]], York, UK.<br /> <br /> [[MLQA 2010|MLQA 2010]], Edinburgh, UK.<br /> <br /> [[MLQA 2011|MLQA 2011]], Aachen, Germany.<br /> <br /> [[MLQA 2012]], Edinburgh, UK.<br /> <br /> <br /> <hr><br /> <br /> <h3 id="speakers">Invited speakers</h3> <br /> <br /> <ul><br /> <li>[http://hs.informatik.uni-oldenburg.de/25665.html Martin Fränzle], University of Oldenburg<br><br /> <em>A tight integration of symbolic, numeric, and statistical methods for the analysis of cyber-physical systems</em></li><br /> <li>[https://sites.google.com/site/zupaolo/ Paolo Zuliani], Newcastle University<br><br /> <em>Statistical Model Checking for Cyber-Physical Systems</em></li><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> <em>Guarding against Denial of Service Attacks</em></li><br /> </ul><br /> <br /> <p>Abstracts of the invited talks are available [[#abstractsLONG|here]].</p><br /> <br /> <br /> <hr><br /> <br /> <h3 id="registration">Registration</h3><br /> <br /> TBA<br /> <br /> <hr><br /> <br /> <h3 id="programme">Preliminary Programme</h3><br /> <br /> TBA<br /> <br /> <hr><br /> <br /> <h3 id="travel">Travel and Accommodation</h3><br /> <br /> <p><br /> TBA<br /> <hr><br /> <br /> <h3 id="organisers">Organiser</h3><br /> <ul><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> </ul><br /> <br /> <hr><br /> <br /> <br /> <div id="minutes"></div><br /> <h3 id="minutess">Minutes</h3><br /> <br /> Minutes of MLQA 2013 will be available after the workshop.<br /> <br /> <br /> <br /> <hr><br /> <br /> <div id="abstractsLONG"></div><h3 id="abstracts">Abstracts of Invited Talks</h3><br /> <br /> <ul><br /> <li>[http://hs.informatik.uni-oldenburg.de/25665.html Martin Fränzle], University of Oldenburg<br><br /> Title: <em>A tight integration of symbolic, numeric, and statistical methods for the analysis of cyber-physical systems</em><br><br /> Abstract: Cyber-physical systems emerge in various application domains, among them<br /> transportation and power networks, provoking a quest for quantitatively<br /> analyzing them with respect to multiple viewpoints, including<br /> functional safety, reliability, and the interaction of the geometric<br /> perspective with the former two. Based on examples from various domains<br /> under different viewpoints, we identify stochastic hybrid systems as a<br /> model able to represent the dynamics relevant to these different<br /> viewpoints. We suggest a symbolic representation of their analysis<br /> problems based on an appropriate hybrid logic and present analysis tools<br /> automatically discharging the proof obligations arising by a blend of<br /> symbolic, safe numeric, and statistical reasoning.<br /> <br /> </li><br /> <li>[https://sites.google.com/site/zupaolo/ Paolo Zuliani], Newcastle University<br><br /> Title: <em>Statistical Model Checking for Cyber-Physical Systems</em><br><br /> Abstract: Statistical model checking is a simulation-based approach for verifying temporal logic properties of complex stochastic systems. Traditional model checking techniques work by searching efficiently the entire state space of the system. However, many interesting systems (e.g., cyber-physical systems) have exceedingly large, or even infinite, state spaces. This makes techniques based on exhaustive search unfeasible. Statistical model checking is instead based on sampling and system simulation, and thereby scales better with system size. We present a statistical model checking approach based on Bayesian statistics, and we apply it to cyber-physical systems coded as Stateflow/Simulink models. Next, we illustrate recent developments involving rare events and non-deterministic systems. We conclude by discussing the strength and weaknesses of the approach and possible directions for future research.<br /> <br><br></li><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> Title: <em>Guarding against Denial of Service Attacks</em><br><br /> Abstract: We outline an approach to the design of systems ensuring that the best possible operation is guaranteed even in the presence of denial of service attacks. As our vehicle of exposition we choose a process calculus allowing to time-out on expected inputs, to base subsequent actions on the extent to which expected inputs were successful and to suitably encrypt the messages exchanged. This is accompanied by an array of analysis techniques for determining the extent to which suitable caution has been exercised: a robustness analysis for ensuring that default data are available when actual data is missing, a safety and security analysis for additionally ensuring that flow of information does not violate integrity models like the Biba model, and a quantitative analysis for determining the probability distributions over the trustworthiness of the data upon which decisions are made.<br /> <br><br></li><br /> </ul></div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=MLQA_2013&diff=453 MLQA 2013 2012-11-27T08:17:13Z

<p>Ender: </p> <hr /> <div><hr><br /> <br /> <h3 id="overivew">Overivew</h3> <br /> The fifth annual meeting of the MLQA working group will take place on Sunday 24 March 2013 as part of the European Joint Conferences on Theory And Practice of Software (ETAPS) in Rome, Italy. This year edition will be held in parallel with the Quantitative Aspects of Programming Languages and Systems (QAPL) workshop. Invited speakers will be shared between the two events.<br /> <br /> <hr><br /> <br /> <h3 id="previous">Past Events</h3> <br /> <br /> [[MLQA 2009|MLQA 2009]], York, UK.<br /> <br /> [[MLQA 2010|MLQA 2010]], Edinburgh, UK.<br /> <br /> [[MLQA 2011|MLQA 2011]], Aachen, Germany.<br /> <br /> [[MLQA 2012]], Edinburgh, UK.<br /> <br /> <br /> <hr><br /> <br /> <h3 id="speakers">Invited speakers</h3> <br /> <br /> <ul><br /> <li>[http://hs.informatik.uni-oldenburg.de/25665.html Martin Fränzle], University of Oldenburg<br><br /> <em>A tight integration of symbolic, numeric, and statistical methods for the analysis of cyber-physical systems</em></li><br /> <li>[https://sites.google.com/site/zupaolo/ Paolo Zuliani], Newcastle University<br><br /> <em>Statistical Model Checking for Cyber-Physical Systems</em></li><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> <em>Guarding against Denial of Service Attacks</em></li><br /> </ul><br /> <br /> <p>Abstracts of the invited talks are available [[#abstractsLONG|here]].</p><br /> <br /> <br /> <hr><br /> <br /> <h3 id="registration">Registration</h3><br /> <br /> TBA<br /> <br /> <hr><br /> <br /> <h3 id="programme">Preliminary Programme</h3><br /> <br /> TBA<br /> <br /> <hr><br /> <br /> <h3 id="travel">Travel and Accommodation</h3><br /> <br /> <p><br /> TBA<br /> <hr><br /> <br /> <h3 id="organisers">Organiser</h3><br /> <ul><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> </ul><br /> <br /> <hr><br /> <br /> <br /> <div id="minutes"></div><br /> <h3 id="minutess">Minutes</h3><br /> <br /> Minutes of MLQA 2013 will be available after the workshop.<br /> <br /> <br /> <br /> <hr><br /> <br /> <div id="abstractsLONG"></div><h3 id="abstracts">Abstracts of Invited Talks</h3><br /> <br /> <ul><br /> <li>[http://hs.informatik.uni-oldenburg.de/25665.html Martin Fränzle], University of Oldenburg<br><br /> Title: <em>A tight integration of symbolic, numeric, and statistical methods for the analysis of cyber-physical systems</em><br><br /> Abstract: Cyber-physical systems emerge in various application domains, among them<br /> transportation and power networks, provoking a quest for quantitatively<br /> analyzing them with respect to multiple viewpoints, including<br /> functional safety, reliability, and the interaction of the geometric<br /> perspective with the former two. Based on examples from various domains<br /> under different viewpoints, we identify stochastic hybrid systems as a<br /> model able to represent the dynamics relevant to these different<br /> viewpoints. We suggest a symbolic representation of their analysis<br /> problems based on an appropriate hybrid logic and present analysis tools<br /> automatically discharging the proof obligations arising by a blend of<br /> symbolic, safe numeric, and statistical reasoning.<br /> <br /> </li><br /> <li>[https://sites.google.com/site/zupaolo/ Paolo Zuliani], Newcastle University<br><br /> Title: <em>Statistical Model Checking for Cyber-Physical Systems</em><br><br /> Abstract: Statistical model checking is a simulation-based approach for verifying temporal logic properties of complex stochastic systems. Traditional model checking techniques work by searching efficiently the entire state space of the system. However, many interesting systems (e.g., cyber-physical systems) have exceedingly large, or even infinite, state spaces. This makes techniques based on exhaustive search unfeasible. Statistical model checking is instead based on sampling and system simulation, and thereby scales better with system size. We present a statistical model checking approach based on Bayesian statistics, and we apply it to cyber-physical systems coded as Stateflow/Simulink models. Next, we illustrate recent developments involving rare events and non-deterministic systems. We conclude by discussing the strength and weaknesses of the approach and possible directions for future research.<br /> <br><br></li><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> Title: <em>Guarding against Denial of Service Attacks</em><br><br /> Abstract: We outline an approach to the design of systems ensuring that the best possible operation is guaranteed even in the presence of denial of service attacks. As our vehicle of exposition we choose a process calculus allowing to time-out on expected inputs, to base subsequent actions on the extent to which expected inputs were successful and to suitably encrypt the messages exchanged. This is accompanied by an array of analysis techniques for determining the extent to which suitable caution has been exercised: a robustness analysis for ensuring that default data are available when actual data is missing, a safety and security analysis for additionally ensuring that flow of information does not violate integrity models like the Biba model, and a quantitative analysis for determining the probability distributions over the trustworthiness of the data upon which decisions are made.<br /> <br><br></li><br /> </ul></div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=MLQA_2013&diff=452 MLQA 2013 2012-11-27T08:15:53Z

<p>Ender: </p> <hr /> <div><br /> <hr><br /> <br /> <h3 id="overivew">Overivew</h3> <br /> The fifth annual meeting of the MLQA working group will take place on Sunday 24 March 2013 as part of the European Joint Conferences on Theory And Practice of Software (ETAPS) in Rome, Italy.<br /> <br /> <hr><br /> <br /> <h3 id="previous">Past Events</h3> <br /> <br /> [[MLQA 2009|MLQA 2009]], York, UK.<br /> <br /> [[MLQA 2010|MLQA 2010]], Edinburgh, UK.<br /> <br /> [[MLQA 2011|MLQA 2011]], Aachen, Germany.<br /> <br /> [[MLQA 2012]], Edinburgh, UK.<br /> <br /> <br /> <hr><br /> <br /> <h3 id="speakers">Invited speakers</h3> <br /> <br /> <ul><br /> <li>[http://hs.informatik.uni-oldenburg.de/25665.html Martin Fränzle], University of Oldenburg<br><br /> <em>A tight integration of symbolic, numeric, and statistical methods for the analysis of cyber-physical systems</em></li><br /> <li>[https://sites.google.com/site/zupaolo/ Paolo Zuliani], Newcastle University<br><br /> <em>Statistical Model Checking for Cyber-Physical Systems</em></li><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> <em>Guarding against Denial of Service Attacks</em></li><br /> </ul><br /> <br /> <p>Abstracts of the invited talks are available [[#abstractsLONG|here]].</p><br /> <br /> <br /> <hr><br /> <br /> <h3 id="registration">Registration</h3><br /> <br /> TBA<br /> <br /> <hr><br /> <br /> <h3 id="programme">Preliminary Programme</h3><br /> <br /> TBA<br /> <br /> <hr><br /> <br /> <h3 id="travel">Travel and Accommodation</h3><br /> <br /> <p><br /> TBA<br /> <hr><br /> <br /> <h3 id="organisers">Organiser</h3><br /> <ul><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> </ul><br /> <br /> <hr><br /> <br /> <br /> <div id="minutes"></div><br /> <h3 id="minutess">Minutes</h3><br /> <br /> Minutes of MLQA 2013 will be available after the workshop.<br /> <br /> <br /> <br /> <hr><br /> <br /> <div id="abstractsLONG"></div><h3 id="abstracts">Abstracts of Invited Talks</h3><br /> <br /> <ul><br /> <li>[http://hs.informatik.uni-oldenburg.de/25665.html Martin Fränzle], University of Oldenburg<br><br /> Title: <em>A tight integration of symbolic, numeric, and statistical methods for the analysis of cyber-physical systems</em><br><br /> Abstract: Cyber-physical systems emerge in various application domains, among them<br /> transportation and power networks, provoking a quest for quantitatively<br /> analyzing them with respect to multiple viewpoints, including<br /> functional safety, reliability, and the interaction of the geometric<br /> perspective with the former two. Based on examples from various domains<br /> under different viewpoints, we identify stochastic hybrid systems as a<br /> model able to represent the dynamics relevant to these different<br /> viewpoints. We suggest a symbolic representation of their analysis<br /> problems based on an appropriate hybrid logic and present analysis tools<br /> automatically discharging the proof obligations arising by a blend of<br /> symbolic, safe numeric, and statistical reasoning.<br /> <br /> </li><br /> <li>[https://sites.google.com/site/zupaolo/ Paolo Zuliani], Newcastle University<br><br /> Title: <em>Statistical Model Checking for Cyber-Physical Systems</em><br><br /> Abstract: Statistical model checking is a simulation-based approach for verifying temporal logic properties of complex stochastic systems. Traditional model checking techniques work by searching efficiently the entire state space of the system. However, many interesting systems (e.g., cyber-physical systems) have exceedingly large, or even infinite, state spaces. This makes techniques based on exhaustive search unfeasible. Statistical model checking is instead based on sampling and system simulation, and thereby scales better with system size. We present a statistical model checking approach based on Bayesian statistics, and we apply it to cyber-physical systems coded as Stateflow/Simulink models. Next, we illustrate recent developments involving rare events and non-deterministic systems. We conclude by discussing the strength and weaknesses of the approach and possible directions for future research.<br /> <br><br></li><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> Title: <em>Guarding against Denial of Service Attacks</em><br><br /> Abstract: We outline an approach to the design of systems ensuring that the best possible operation is guaranteed even in the presence of denial of service attacks. As our vehicle of exposition we choose a process calculus allowing to time-out on expected inputs, to base subsequent actions on the extent to which expected inputs were successful and to suitably encrypt the messages exchanged. This is accompanied by an array of analysis techniques for determining the extent to which suitable caution has been exercised: a robustness analysis for ensuring that default data are available when actual data is missing, a safety and security analysis for additionally ensuring that flow of information does not violate integrity models like the Biba model, and a quantitative analysis for determining the probability distributions over the trustworthiness of the data upon which decisions are made.<br /> <br><br></li><br /> </ul></div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=MLQA_2013&diff=451 MLQA 2013 2012-11-27T08:15:13Z

<p>Ender: </p> <hr /> <div><br /> <br /> <hr><br /> <br /> <h3 id="overivew">Overivew</h3> <br /> The fifth annual meeting of the MLQA working group will take place on Sunday 24 March 2013 as part of the European Joint Conferences on Theory And Practice of Software (ETAPS) in Rome, Italy.<br /> <br /> <hr><br /> <br /> <h3 id="previous">Past Events</h3> <br /> <br /> [[MLQA 2009|MLQA 2009]], York, UK.<br /> <br /> [[MLQA 2010|MLQA 2010]], Edinburgh, UK.<br /> <br /> [[MLQA 2011|MLQA 2011]], Aachen, Germany.<br /> <br /> [[MLQA 2012]], Edinburgh, UK.<br /> <br /> <br /> <hr><br /> <br /> <h3 id="speakers">Invited speakers</h3> <br /> <br /> <ul><br /> <li>[http://hs.informatik.uni-oldenburg.de/25665.html Martin Fränzle], University of Oldenburg<br><br /> <em>A tight integration of symbolic, numeric, and statistical methods for the analysis of cyber-physical systems</em></li><br /> <li>[https://sites.google.com/site/zupaolo/ Paolo Zuliani], Newcastle University<br><br /> <em>Statistical Model Checking for Cyber-Physical Systems</em></li><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> <em>Guarding against Denial of Service Attacks</em></li><br /> </ul><br /> <br /> <p>Abstracts of the invited talks are available [[#abstractsLONG|here]].</p><br /> <br /> <br /> <hr><br /> <br /> <h3 id="registration">Registration</h3><br /> <br /> TBA<br /> <br /> <hr><br /> <br /> <h3 id="programme">Preliminary Programme</h3><br /> <br /> TBA<br /> <br /> <hr><br /> <br /> <h3 id="travel">Travel and Accommodation</h3><br /> <br /> <p><br /> TBA<br /> <hr><br /> <br /> <h3 id="organisers">Organisers</h3><br /> <ul><br /> <li>[http://homepages.inf.ed.ac.uk/jeh/ Jane Hilston], University of Edinburgh</li><br /> <li>[http://www.dcs.gla.ac.uk/people/personal/gethin/ Gethin Norman], University of Glasgow</li><br /> </ul><br /> <br /> <hr><br /> <br /> <br /> <div id="minutes"></div><br /> <h3 id="minutess">Minutes</h3><br /> <br /> Minutes of MLQA 2013 will be available after the workshop.<br /> <br /> <br /> <br /> <hr><br /> <br /> <div id="abstractsLONG"></div><h3 id="abstracts">Abstracts of Invited Talks</h3><br /> <br /> <ul><br /> <li>[http://hs.informatik.uni-oldenburg.de/25665.html Martin Fränzle], University of Oldenburg<br><br /> Title: <em>A tight integration of symbolic, numeric, and statistical methods for the analysis of cyber-physical systems</em><br><br /> Abstract: Cyber-physical systems emerge in various application domains, among them<br /> transportation and power networks, provoking a quest for quantitatively<br /> analyzing them with respect to multiple viewpoints, including<br /> functional safety, reliability, and the interaction of the geometric<br /> perspective with the former two. Based on examples from various domains<br /> under different viewpoints, we identify stochastic hybrid systems as a<br /> model able to represent the dynamics relevant to these different<br /> viewpoints. We suggest a symbolic representation of their analysis<br /> problems based on an appropriate hybrid logic and present analysis tools<br /> automatically discharging the proof obligations arising by a blend of<br /> symbolic, safe numeric, and statistical reasoning.<br /> <br /> </li><br /> <li>[https://sites.google.com/site/zupaolo/ Paolo Zuliani], Newcastle University<br><br /> Title: <em>Statistical Model Checking for Cyber-Physical Systems</em><br><br /> Abstract: Statistical model checking is a simulation-based approach for verifying temporal logic properties of complex stochastic systems. Traditional model checking techniques work by searching efficiently the entire state space of the system. However, many interesting systems (e.g., cyber-physical systems) have exceedingly large, or even infinite, state spaces. This makes techniques based on exhaustive search unfeasible. Statistical model checking is instead based on sampling and system simulation, and thereby scales better with system size. We present a statistical model checking approach based on Bayesian statistics, and we apply it to cyber-physical systems coded as Stateflow/Simulink models. Next, we illustrate recent developments involving rare events and non-deterministic systems. We conclude by discussing the strength and weaknesses of the approach and possible directions for future research.<br /> <br><br></li><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> Title: <em>Guarding against Denial of Service Attacks</em><br><br /> Abstract: We outline an approach to the design of systems ensuring that the best possible operation is guaranteed even in the presence of denial of service attacks. As our vehicle of exposition we choose a process calculus allowing to time-out on expected inputs, to base subsequent actions on the extent to which expected inputs were successful and to suitably encrypt the messages exchanged. This is accompanied by an array of analysis techniques for determining the extent to which suitable caution has been exercised: a robustness analysis for ensuring that default data are available when actual data is missing, a safety and security analysis for additionally ensuring that flow of information does not violate integrity models like the Biba model, and a quantitative analysis for determining the probability distributions over the trustworthiness of the data upon which decisions are made.<br /> <br><br></li><br /> </ul></div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=MLQA_2013&diff=450 MLQA 2013 2012-11-27T08:13:54Z

<p>Ender: </p> <hr /> <div><br /> <br /> <br /> <hr><br /> <br /> <h3 id="overivew">Overivew</h3> <br /> The fifth annual meeting of the MLQA working group will take place on Sunday 24 March 2013 as part of the European Joint Conferences on Theory And Practice of Software (ETAPS) in Rome, Italy.<br /> <br /> <hr><br /> <br /> <h3 id="previous">Past Events</h3> <br /> <br /> [[MLQA 2009|MLQA 2009]], York, UK.<br /> <br /> [[MLQA 2010|MLQA 2010]], Edinburgh, UK.<br /> <br /> [[MLQA 2011|MLQA 2011]], Aachen, Germany.<br /> <br /> [[MLQA 2012]], Edinburgh, UK.<br /> <br /> <br /> <hr><br /> <br /> <h3 id="speakers">Invited speakers</h3> <br /> <br /> <ul><br /> <li>[http://hs.informatik.uni-oldenburg.de/25665.html Martin Fränzle], University of Oldenburg<br><br /> <em>A tight integration of symbolic, numeric, and statistical methods for the analysis of cyber-physical systems</em></li><br /> <li>[https://sites.google.com/site/zupaolo/ Paolo Zuliani], Newcastle University<br><br /> <em>Statistical Model Checking for Cyber-Physical Systems</em></li><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> <em>Guarding against Denial of Service Attacks</em></li><br /> </ul><br /> <br /> <p>Abstracts of the invited talks are available [[#abstractsLONG|here]].</p><br /> <br /> <br /> <hr><br /> <br /> <h3 id="registration">Registration</h3><br /> <br /> TBA<br /> <br /> <hr><br /> <br /> <h3 id="programme">Preliminary Programme</h3><br /> <br /> TBA<br /> <br /> <hr><br /> <br /> <h3 id="travel">Travel and Accommodation</h3><br /> <br /> <p><br /> TBA<br /> <hr><br /> <br /> <br /> <br /> <br /> <div id="minutes"></div><br /> <h3 id="minutess">Minutes</h3><br /> <br /> Minutes of MLQA 2013 will be available after the workshop.<br /> <br /> <br /> <br /> <hr><br /> <br /> <div id="abstractsLONG"></div><h3 id="abstracts">Abstracts of Invited Talks</h3><br /> <br /> <ul><br /> <li>[http://hs.informatik.uni-oldenburg.de/25665.html Martin Fränzle], University of Oldenburg<br><br /> Title: <em>A tight integration of symbolic, numeric, and statistical methods for the analysis of cyber-physical systems</em><br><br /> Abstract: Cyber-physical systems emerge in various application domains, among them<br /> transportation and power networks, provoking a quest for quantitatively<br /> analyzing them with respect to multiple viewpoints, including<br /> functional safety, reliability, and the interaction of the geometric<br /> perspective with the former two. Based on examples from various domains<br /> under different viewpoints, we identify stochastic hybrid systems as a<br /> model able to represent the dynamics relevant to these different<br /> viewpoints. We suggest a symbolic representation of their analysis<br /> problems based on an appropriate hybrid logic and present analysis tools<br /> automatically discharging the proof obligations arising by a blend of<br /> symbolic, safe numeric, and statistical reasoning.<br /> <br /> </li><br /> <li>[https://sites.google.com/site/zupaolo/ Paolo Zuliani], Newcastle University<br><br /> Title: <em>Statistical Model Checking for Cyber-Physical Systems</em><br><br /> Abstract: Statistical model checking is a simulation-based approach for verifying temporal logic properties of complex stochastic systems. Traditional model checking techniques work by searching efficiently the entire state space of the system. However, many interesting systems (e.g., cyber-physical systems) have exceedingly large, or even infinite, state spaces. This makes techniques based on exhaustive search unfeasible. Statistical model checking is instead based on sampling and system simulation, and thereby scales better with system size. We present a statistical model checking approach based on Bayesian statistics, and we apply it to cyber-physical systems coded as Stateflow/Simulink models. Next, we illustrate recent developments involving rare events and non-deterministic systems. We conclude by discussing the strength and weaknesses of the approach and possible directions for future research.<br /> <br><br></li><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> Title: <em>Guarding against Denial of Service Attacks</em><br><br /> Abstract: We outline an approach to the design of systems ensuring that the best possible operation is guaranteed even in the presence of denial of service attacks. As our vehicle of exposition we choose a process calculus allowing to time-out on expected inputs, to base subsequent actions on the extent to which expected inputs were successful and to suitably encrypt the messages exchanged. This is accompanied by an array of analysis techniques for determining the extent to which suitable caution has been exercised: a robustness analysis for ensuring that default data are available when actual data is missing, a safety and security analysis for additionally ensuring that flow of information does not violate integrity models like the Biba model, and a quantitative analysis for determining the probability distributions over the trustworthiness of the data upon which decisions are made.<br /> <br><br></li><br /> </ul></div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=MLQA_2013&diff=449 MLQA 2013 2012-11-27T08:05:12Z

<p>Ender: </p> <hr /> <div>The fifth annual meeting of the MLQA working group will take place on Sunday 24 March 2013 as part of the European Joint Conferences on Theory And Practice of Software (ETAPS) in Rome, Italy. The details of the meeting will be posted on this page soon.<br /> <br /> <br /> <hr><br /> <br /> <h3 id="speakers">Invited speakers</h3> <br /> <br /> <ul><br /> <li>[http://hs.informatik.uni-oldenburg.de/25665.html Martin Fränzle], University of Oldenburg<br><br /> <em>A tight integration of symbolic, numeric, and statistical methods for the analysis of cyber-physical systems</em></li><br /> <li>[https://sites.google.com/site/zupaolo/ Paolo Zuliani], Newcastle University<br><br /> <em>Statistical Model Checking for Cyber-Physical Systems</em></li><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> <em>Guarding against Denial of Service Attacks</em></li><br /> </ul><br /> <br /> <p>Abstracts of the invited talks are available [[#abstractsLONG|here]].</p><br /> <br /> <br /> <hr><br /> <br /> <h3 id="registration">Registration</h3><br /> <br /> TBA<br /> <br /> <hr><br /> <br /> <h3 id="programme">Preliminary Programme</h3><br /> <br /> TBA<br /> <br /> <hr><br /> <br /> <h3 id="travel">Travel and Accommodation</h3><br /> <br /> <p><br /> TBA<br /> <hr><br /> <br /> <br /> <br /> <br /> <div id="minutes"></div><br /> <h3 id="minutess">Minutes</h3><br /> <br /> Minutes of MLQA 2013 will be available after the workshop.<br /> <br /> <br /> <br /> <hr><br /> <br /> <div id="abstractsLONG"></div><h3 id="abstracts">Abstracts of Invited Talks</h3><br /> <br /> <ul><br /> <li>[http://hs.informatik.uni-oldenburg.de/25665.html Martin Fränzle], University of Oldenburg<br><br /> Title: <em>A tight integration of symbolic, numeric, and statistical methods for the analysis of cyber-physical systems</em><br><br /> Abstract: Cyber-physical systems emerge in various application domains, among them<br /> transportation and power networks, provoking a quest for quantitatively<br /> analyzing them with respect to multiple viewpoints, including<br /> functional safety, reliability, and the interaction of the geometric<br /> perspective with the former two. Based on examples from various domains<br /> under different viewpoints, we identify stochastic hybrid systems as a<br /> model able to represent the dynamics relevant to these different<br /> viewpoints. We suggest a symbolic representation of their analysis<br /> problems based on an appropriate hybrid logic and present analysis tools<br /> automatically discharging the proof obligations arising by a blend of<br /> symbolic, safe numeric, and statistical reasoning.<br /> <br /> </li><br /> <li>[https://sites.google.com/site/zupaolo/ Paolo Zuliani], Newcastle University<br><br /> Title: <em>Statistical Model Checking for Cyber-Physical Systems</em><br><br /> Abstract: Statistical model checking is a simulation-based approach for verifying temporal logic properties of complex stochastic systems. Traditional model checking techniques work by searching efficiently the entire state space of the system. However, many interesting systems (e.g., cyber-physical systems) have exceedingly large, or even infinite, state spaces. This makes techniques based on exhaustive search unfeasible. Statistical model checking is instead based on sampling and system simulation, and thereby scales better with system size. We present a statistical model checking approach based on Bayesian statistics, and we apply it to cyber-physical systems coded as Stateflow/Simulink models. Next, we illustrate recent developments involving rare events and non-deterministic systems. We conclude by discussing the strength and weaknesses of the approach and possible directions for future research.<br /> <br><br></li><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> Title: <em>Guarding against Denial of Service Attacks</em><br><br /> Abstract: We outline an approach to the design of systems ensuring that the best possible operation is guaranteed even in the presence of denial of service attacks. As our vehicle of exposition we choose a process calculus allowing to time-out on expected inputs, to base subsequent actions on the extent to which expected inputs were successful and to suitably encrypt the messages exchanged. This is accompanied by an array of analysis techniques for determining the extent to which suitable caution has been exercised: a robustness analysis for ensuring that default data are available when actual data is missing, a safety and security analysis for additionally ensuring that flow of information does not violate integrity models like the Biba model, and a quantitative analysis for determining the probability distributions over the trustworthiness of the data upon which decisions are made.<br /> <br><br></li><br /> </ul></div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=MLQA_2013&diff=448 MLQA 2013 2012-11-26T14:02:25Z

<p>Ender: </p> <hr /> <div>The fifth annual meeting of the MLQA working group will take place on Sunday 24 March 2013 as part of the European Joint Conferences on Theory And Practice of Software (ETAPS) in Rome, Italy. The details of the meeting will be posted on this page soon.<br /> <br /> <br /> <hr><br /> <br /> <h3 id="speakers">Invited speakers</h3> <br /> <br /> <ul><br /> <li>[http://hs.informatik.uni-oldenburg.de/25665.html Martin Fränzle], University of Oldenburg<br><br /> <em>To be announced</em></li><br /> <li>[https://sites.google.com/site/zupaolo/ Paolo Zuliani], Newcastle University<br><br /> <em>Statistical Model Checking for Cyber-Physical Systems</em></li><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> <em>Guarding against Denial of Service Attacks</em></li><br /> </ul><br /> <br /> <p>Abstracts of the invited talks are available [[#abstractsLONG|here]].</p><br /> <br /> <br /> <hr><br /> <br /> <h3 id="registration">Registration</h3><br /> <br /> TBA<br /> <br /> <hr><br /> <br /> <h3 id="programme">Preliminary Programme</h3><br /> <br /> TBA<br /> <br /> <hr><br /> <br /> <h3 id="travel">Travel and Accommodation</h3><br /> <br /> <p><br /> TBA<br /> <hr><br /> <br /> <br /> <br /> <br /> <div id="minutes"></div><br /> <h3 id="minutess">Minutes</h3><br /> <br /> Minutes of MLQA 2013 will be available after the workshop.<br /> <br /> <br /> <br /> <hr><br /> <br /> <div id="abstractsLONG"></div><h3 id="abstracts">Abstracts of Invited Talks</h3><br /> <br /> <ul><br /> <li>[http://hs.informatik.uni-oldenburg.de/25665.html Martin Fränzle], University of Oldenburg<br><br /> Title: <em>To be announced</em><br><br /> Abstract: To be announced.<br /> <br /> </li><br /> <li>[https://sites.google.com/site/zupaolo/ Paolo Zuliani], Newcastle University<br><br /> Title: <em>Statistical Model Checking for Cyber-Physical Systems</em><br><br /> Abstract: Statistical model checking is a simulation-based approach for verifying temporal logic properties of complex stochastic systems. Traditional model checking techniques work by searching efficiently the entire state space of the system. However, many interesting systems (e.g., cyber-physical systems) have exceedingly large, or even infinite, state spaces. This makes techniques based on exhaustive search unfeasible. Statistical model checking is instead based on sampling and system simulation, and thereby scales better with system size. We present a statistical model checking approach based on Bayesian statistics, and we apply it to cyber-physical systems coded as Stateflow/Simulink models. Next, we illustrate recent developments involving rare events and non-deterministic systems. We conclude by discussing the strength and weaknesses of the approach and possible directions for future research.<br /> <br><br></li><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> Title: <em>Guarding against Denial of Service Attacks</em><br><br /> Abstract: We outline an approach to the design of systems ensuring that the best possible operation is guaranteed even in the presence of denial of service attacks. As our vehicle of exposition we choose a process calculus allowing to time-out on expected inputs, to base subsequent actions on the extent to which expected inputs were successful and to suitably encrypt the messages exchanged. This is accompanied by an array of analysis techniques for determining the extent to which suitable caution has been exercised: a robustness analysis for ensuring that default data are available when actual data is missing, a safety and security analysis for additionally ensuring that flow of information does not violate integrity models like the Biba model, and a quantitative analysis for determining the probability distributions over the trustworthiness of the data upon which decisions are made.<br /> <br><br></li><br /> </ul></div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=MLQA_2013&diff=447 MLQA 2013 2012-11-26T13:36:30Z

<p>Ender: </p> <hr /> <div>The fifth annual meeting of the MLQA working group will take place on Sunday 24 March 2013 as part of the European Joint Conferences on Theory And Practice of Software (ETAPS) in Rome, Italy. The details of the meeting will be posted on this page soon.<br /> <br /> <br /> <hr><br /> <br /> <h3 id="speakers">Invited speakers</h3> <br /> <br /> <ul><br /> <li>[http://hs.informatik.uni-oldenburg.de/25665.html Martin Fränzle], University of Oldenburg<br><br /> <em>To be announced</em></li><br /> <li>[https://sites.google.com/site/zupaolo/ Paolo Zuliani], Newcastle University<br><br /> <em>Statistical Model Checking for Cyber-Physical Systems</em></li><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> <em>Guarding against Denial of Service Attacks</em></li><br /> </ul><br /> <br /> <p>Abstracts of the invited talks are available [[#abstractsLONG|here]].</p><br /> <br /> <hr><br /> <br /> <div id="abstractsLONG"></div><h3 id="abstracts">Abstracts of Invited Talks</h3><br /> <br /> <ul><br /> <li>[http://hs.informatik.uni-oldenburg.de/25665.html Martin Fränzle], University of Oldenburg<br><br /> Title: <em>To be announced</em><br><br /> Abstract: To be announced.<br /> <br /> </li><br /> <li>[https://sites.google.com/site/zupaolo/ Paolo Zuliani], Newcastle University<br><br /> Title: <em>Statistical Model Checking for Cyber-Physical Systems</em><br><br /> Abstract: Statistical model checking is a simulation-based approach for verifying temporal logic properties of complex stochastic systems. Traditional model checking techniques work by searching efficiently the entire state space of the system. However, many interesting systems (e.g., cyber-physical systems) have exceedingly large, or even infinite, state spaces. This makes techniques based on exhaustive search unfeasible. Statistical model checking is instead based on sampling and system simulation, and thereby scales better with system size. We present a statistical model checking approach based on Bayesian statistics, and we apply it to cyber-physical systems coded as Stateflow/Simulink models. Next, we illustrate recent developments involving rare events and non-deterministic systems. We conclude by discussing the strength and weaknesses of the approach and possible directions for future research.<br /> <br><br></li><br /> <li>[http://www.imm.dtu.dk/~nielson Flemming Nielson], Technical University of Denmark<br><br /> Title: <em>Guarding against Denial of Service Attacks</em><br><br /> Abstract: We outline an approach to the design of systems ensuring that the best possible operation is guaranteed even in the presence of denial of service attacks. As our vehicle of exposition we choose a process calculus allowing to time-out on expected inputs, to base subsequent actions on the extent to which expected inputs were successful and to suitably encrypt the messages exchanged. This is accompanied by an array of analysis techniques for determining the extent to which suitable caution has been exercised: a robustness analysis for ensuring that default data are available when actual data is missing, a safety and security analysis for additionally ensuring that flow of information does not violate integrity models like the Biba model, and a quantitative analysis for determining the probability distributions over the trustworthiness of the data upon which decisions are made.<br /> <br><br></li><br /> </ul></div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=Main_Page&diff=446 Main Page 2012-11-13T08:55:09Z

<p>Ender: </p> <hr /> <div>== ERCIM Working Group on Models and Logics for Quantitative Analysis (MLQA) ==<br /> <br /> [[Image:Image002.png|frame]] Models and Logics for Quantitative Analysis are seen as comprising process models analysed using logics for quantitative properties. More specifically, we will<br /> <br /> # consider process models formally described by transition systems, automata or process calculi,<br /> # consider logics for expressing stochastic and continuous properties as well as discrete ones,<br /> # focus on algorithms, theory and tools, and<br /> # study applications with particular emphasis on embedded systems and service oriented systems but will aim at treating also IT guided workflow systems and biological systems.<br /> <br /> The MLQA home page: http://wiki.ercim.eu/wg/MLQA<br /> <br /> The goal of this working group is to create a venue for knowledge sharing in this exciting area, for creating a network also for young researchers, for sharing tools developed within the field, for discussing research directions, and eventually to formulate a European project or network on formal quantitative analysis.<br /> <br /> The working group will be open also to researchers outside of ERCIM (and outside of Europe).<br /> <br /> == Upcoming events ==<br /> <br /> <span style="color: red;">The fifth annual meeting: [[MLQA 2013]], Rome, Italy.</span><br /> <br /> == Past events ==<br /> <br /> The Kick-Off meeting: [[MLQA 2009|MLQA 2009]], York, UK.<br /> <br /> The second annual meeting: [[MLQA 2010|MLQA 2010]], Edinburgh, UK.<br /> <br /> The third annual meeting: [[MLQA 2011|MLQA 2011]], Aachen, Germany.<br /> <br /> The fourth annual meeting: [[MLQA 2012]], Edinburgh, UK.</div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=MLQA_2012&diff=445 MLQA 2012 2012-09-12T14:31:46Z

<p>Ender: </p> <hr /> <div><table width="100%" border="0"><br /> <tr><br /> <td><br /> <h1>Joint Workshop on Compositional Modelling and Analysis of Quantitative Systems</h1><br /> <b>September 8, 2012</b><br /> <b>University of Edinburgh</b><br /> </td><br /> <td>&nbsp;</td><br /> <td align="right"><br /> <table width="100%" border="0"><br /> <tr><br /> <td align="right"><br />  </td><br /> </tr></table><br /> [[File:Sicsa.jpg|link=http://www.sicsa.ac.uk/themes/modelling-and-abstraction]]<br /> </td><br /> </tr><br /> </table><br /> <br /> __TOC__<br /> <br /> <hr><br /> <br /> <h3 id="overview">Overview</h3><br /> <br /> <p><br /> The workshop combines the Fourth annual meeting of the [http://wiki.ercim.eu/wg/MLQA ERCIM Working Group on Models and Logics for Quantitative Analysis (MLQA)] with a [http://www.sicsa.ac.uk/themes/modelling-and-abstraction SICSA Modelling and Abstraction Theme] event.<br /> </p><br /> <br /> <p><br /> The theme of the workshop is <em>Compositional Modelling and Analysis of Quantitative Systems</em>. Compositionality is a key concept in both the modeling and analysis of computer systems. It is only by decomposing large complex system into smaller pieces, we can build and analyse these systems.<br /> </p><br /> <br /> <p><br /> The aim of the workshop is to bring together researchers working on quantitative modelling and analysis of computer systems focusing on research using compositional techniques. The workshop hopes to encourage interaction and collaboration between the attendees in developing compositional approaches. <br /> The workshop will bring together MLQA participants from across Europe with contributors to the SICSA theme of 'Modelling and Abstraction'. However, participation from outside MLQA and the SICSA theme are also welcome. <br /> </p><br /> <br /> <p><br /> The workshop will take place immediately following the [http://conferences.ncl.ac.uk/concur-2012/ CONCUR International Conference] taking place in Newcastle-upon-Tyne<br /> 4-7th September 2012.<br /> </p> <br /> <br /> <hr><br /> <br /> <h3 id="speakers">Invited speakers</h3> <br /> <br /> <ul><br /> <li>[http://cs.famaf.unc.edu.ar/~dargenio/ Pedro D'Argenio], FaMAF, Universidad Nacional de Cordoba<br /> <br><br /> <em>Security analysis in probabilistic distributed protocols via bounded reachability</em><br /> </li><br /> <li>[http://www.dsi.unive.it/~marin/ Andrea Marin], Universita di Venezia<br><br /> <em>Compositional model specifications and analyses via product-forms</em></li><br /> <li>[http://wwwhome.cs.utwente.nl/~vdpol/ Jaco van de Pol], University of Twente<br /> <br><br /> <em>Symbolic manipulation of markov automata</em><br /> </li><br /> <li>[http://www.pst.ifi.lmu.de/people/staff/tribastone/ Mirco Tribastone], Ludwig-Maximilians-Universit&#228;t M&#252;nchen <br /> <br><br /> <em>Exact aggregation for fluid process algebra models</em><br /> </li><br /> </ul><br /> <br /> <p><br /> Abstracts of the invited talks are available [[#abstractsX|here]].<br /> </p><br /> <br /> <hr><br /> <br /> <h3 id="registration">Registration</h3><br /> <br /> <p><br /> Registration will be at a cost of £25. Registration is free for members of SICSA institutions.<br><br /> Registration is available through the [http://www.epay.ed.ac.uk/browse/extra_info.asp?compid=1&catid=42&modid=2&prodid=795&deptid=24&prodvarid=0 online registration system].<br /> </p><br /> <br /> <hr><br /> <br /> <h3 id="posters">Posters</h3><br /> <br /> <p><br /> We invited posters under two categories:<br /> </p><br /> <br /> <ul><li><br /> Presentation of recent or on-going work in relation to the themes of MLQA.<br /> </li><br /> <li><br /> Overview of the recent research activities of a research group related to the themes of MLQA.<br /> </li><br /> </ul><br /> <br /> <p><br /> We equally encourage submissions from both research leaders, junior researchers and PhD students.<br /> </p><br /> <br /> <p><br /> Posters should be printed by the <em>participants</em> in their preferred size.<br /> </p><br /> <br /> <p><br /> Notification of your intention to submit, along with a title and short description of the poster, should be sent by <b>August 31</b> to [mailto:gethin.norman@glasgow.ac.uk gethin.norman@glasgow.ac.uk].<br /> </p><br /> <br /> <hr><br /> <br /> <h3 id="programme">Preliminary Programme</h3><br /> <br /> <ul><br /> <li>09:30 - 09:45 <em>Opening</em><br /> </li><br /> <li>09:45 - 10:30 <em>invited talk</em><br /> <br><br><br /> </li><br /> <li>10:30 - 11:00 <em>coffee</em><br /> <br><br><br /> </li><br /> <li>11:00 - 11:45 <em>Invited talk</em><br /> </li><br /> <li>11:45 - 12:30 <em>Invited talk</em><br /> <br><br><br /> </li><br /> <li>12:30 - 14:00 <em>lunch & poster session</em><br /> <br><br><br /> </li><br /> <li>14:00 - 14:30 <em>SICSA Contributed talk</em><br /> </li><br /> <li>14:30 - 15:00 <em>SICSA Contributed talk</em><br /> </li><br /> <li>15:00 - 15:30 <em>SICSA Contributed talk</em><br /> <br><br><br /> </li><br /> <li>15:30 - 16:00 <em>coffee</em><br /> <br><br><br /> </li><br /> <li>16:00 - 17:00 <em>MLQA business meeting</em><br /> </li><br /> </ul><br /> <br /> <hr><br /> <br /> <h3 id="travel">Travel and Accommodation</h3><br /> <br /> <p><br /> The workshop will take place at the<br /> Informatics Forum of the School of Informatics, University of Edinburgh. For details on its location as well as links for travel directions see [http://www.ed.ac.uk/schools-departments/informatics/about/location here]. For those attending CONCUR, Edinburgh is approximately 90 minutes from Newcastle by train.<br /> </p><br /> <br /> <p><br /> For information regarding accommodation will be available soon.<br /> <hr><br /> <br /> <h3 id="organisers">Organisers</h3><br /> <ul><br /> <li>[http://homepages.inf.ed.ac.uk/jeh/ Jane Hilston], University of Edinburgh</li><br /> <li>[http://www.dcs.gla.ac.uk/people/personal/gethin/ Gethin Norman], University of Glasgow</li><br /> </ul><br /> <br /> <hr><br /> <br /> <div id="abstractsX"></div><br /> <h3 id="abstracts">Abstracts of Invited Talks</h3><br /> <br /> <ul><br /> <li>[http://cs.famaf.unc.edu.ar/~dargenio/ Pedro D'Argenio], FaMAF, Universidad Nacional de Cordoba<br /> <br><br /> Title: <em>Security analysis in probabilistic distributed protocols via bounded reachability.<br /> </em><br><br /> Abstract: Probabilistic model checking computes the probability values of a given property quantifying over all possible schedulers (also known as adversaries or policies). It turns out that maximum and minimum probabilities calculated in such a way are overestimations on models of distributed systems in which components are loosely coupled and share little information with each other. The problem exacerbates, if n addition the system is intended to protect private information.<br /> <br><br><br /> In this talk, we will (1) discuss the problem, (2) give a characterization for the set of schedulers that respect the distributed nature of process and the idea of secrecy, (3) report of some important properties of this class of schedulers, and (4) present an algorithm to analyze time-bounded reachability properties based on polynomial optimization. We will briefly discuss a prototype implementation and report some case studies.<br /> <br><br></li><br /> <li>[http://www.dsi.unive.it/~marin/ Andrea Marin], Universita di Venezia<br /> <br><br /> Title: <em>Compositional model specifications and analyses via product-forms</em><br><br /> Abstract: Compositionality is an important aspect of many formalisms used for<br /> quantitative analysis of computer software and hardware architectures<br /> and communication systems. Compositionality allows for the specification <br /> of complex models in terms of cooperations of simpler components in<br /> a modular and hierarchical way. <br /> <br><br><br /> However, these elegant and often compact model definitions often hide<br /> a huge complexity in the structure of the state space. For models with<br /> underlying continuous or discrete time Markov chains this implies that the quantitative<br /> evaluation of performance and reliability indices cannot rely on<br /> brute force approaches (such as the solution of the set of global balance<br /> equations). Therefore, from the point of view of the<br /> quantitative analysis of compositional models, an approach<br /> that allows one to tackle large state spaces is needed. When<br /> the models are characterised by underlying continuous time Markov<br /> chains (e.g., stochastic Petri nets, Performance Evaluation Process algebra -PEPA-) <br /> product-form theory may be successfully applied. Informally, product-forms<br /> aim at studying the model properties in steady-state starting from the<br /> analysis of its isolated components which are opportunely "parametrised" in order<br /> to take into account the interactions with the remaining parts of the model. <br /> <br><br><br /> After introducing product-form theory in stochastic process algebra<br /> domain, the talk will address the problem of deciding if product-form conditions<br /> are satisfied by the composition of a set of components and how the parameterisation<br /> of these components can be achieved. Special attention will be devoted to the<br /> automation of these steps even in cases of models with infinite state spaces.<br /> The Iterative Numerical Algorithm for Product-forms will be presented. <br /> Concluding remarks will consider the problem of the computation of the <br /> normalising constant and product-form approximations.<br /> <br><br><br /> </li><br /> <li>[http://wwwhome.cs.utwente.nl/~vdpol/ Jaco van de Pol], University of Twente<br /> <br><br /> Title: <em>Symbolic Manipulation of Markov Automata</em><br><br /> Abstract: Markov automata combine non-deterministic choice, probabilistic choice,<br /> and stochastic delays, and come with a natural notion of parallel composition.<br /> Since these automata generalize labeled transition systems and both<br /> discrete-time and continuous-time Markov Chains, they provide a rich<br /> model of computation.<br /> <br><br><br /> We will present the process algebra MAPA for specifying Markov Automata<br /> in a symbolic manner. Specifications in MAPA can be very concise, due to<br /> parallel composition and the use of data types. MAPA specifications can<br /> be transformed into a linear process format, which is an excellent basis<br /> for symbolic transformation and optimization of Markov Automata.<br /> <br><br></li> <br /> <li>[http://www.pst.ifi.lmu.de/people/staff/tribastone/ Mirco Tribastone], Ludwig-Maximilians-Universit&#228;t M&#252;nchen <br /> <br><br /> Title: <em>Exact Aggregation for Fluid Process Algebra Models</em><br><br /> Abstract: Recent research in stochastic process algebra has led to efficient fluid approximation techniques obtained by aggregating large populations of sequential components into a single continuous-state variable represented as an ordinary differential equation (ODE). In this talk I will show that, when aggregation is performed higher up in the syntax tree of a model --- i.e., when one is interested in replicas of composite processes --- the resulting ODE system does not scale well with population sizes. I will present two techniques to tackle this problem. The first one is a model-to-model transformation at the process-algebra level. It converts a model with a large ODE system into another one whose size is independent from all population levels, but whose solution is related exactly to that of the original system. Simple syntactic checks are a necessary condition for this transformation to be carried out. The second technique enlarges the class of models amenable to exact aggregation. It performs a transformation directly at the level of the underlying ODE system, which is induced by a novel notion of behavioural equivalence for process algebra with fluid semantics. <br /> </li><br /> </ul><br /> <br /> <br /> <hr><br /> <br /> <div id="minutes"></div><br /> <h3 id="minutess">Minutes</h3><br /> <br /> Minutes of MLQA 2012 is avaliable [http://wiki.ercim.eu/wg/MLQA/images/8/80/Minutes_from_the_MLQA_2012_Meeting.pdf here].</div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=File:Minutes_from_the_MLQA_2012_Meeting.pdf&diff=444 File:Minutes from the MLQA 2012 Meeting.pdf 2012-09-12T14:30:51Z

<p>Ender: </p> <hr /> <div></div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=MLQA_2012&diff=443 MLQA 2012 2012-09-12T14:29:17Z

<p>Ender: </p> <hr /> <div><table width="100%" border="0"><br /> <tr><br /> <td><br /> <h1>Joint Workshop on Compositional Modelling and Analysis of Quantitative Systems</h1><br /> <b>September 8, 2012</b><br /> <b>University of Edinburgh</b><br /> </td><br /> <td>&nbsp;</td><br /> <td align="right"><br /> <table width="100%" border="0"><br /> <tr><br /> <td align="right"><br />  </td><br /> </tr></table><br /> [[File:Sicsa.jpg|link=http://www.sicsa.ac.uk/themes/modelling-and-abstraction]]<br /> </td><br /> </tr><br /> </table><br /> <br /> __TOC__<br /> <br /> <hr><br /> <br /> <h3 id="overview">Overview</h3><br /> <br /> <p><br /> The workshop combines the Fourth annual meeting of the [http://wiki.ercim.eu/wg/MLQA ERCIM Working Group on Models and Logics for Quantitative Analysis (MLQA)] with a [http://www.sicsa.ac.uk/themes/modelling-and-abstraction SICSA Modelling and Abstraction Theme] event.<br /> </p><br /> <br /> <p><br /> The theme of the workshop is <em>Compositional Modelling and Analysis of Quantitative Systems</em>. Compositionality is a key concept in both the modeling and analysis of computer systems. It is only by decomposing large complex system into smaller pieces, we can build and analyse these systems.<br /> </p><br /> <br /> <p><br /> The aim of the workshop is to bring together researchers working on quantitative modelling and analysis of computer systems focusing on research using compositional techniques. The workshop hopes to encourage interaction and collaboration between the attendees in developing compositional approaches. <br /> The workshop will bring together MLQA participants from across Europe with contributors to the SICSA theme of 'Modelling and Abstraction'. However, participation from outside MLQA and the SICSA theme are also welcome. <br /> </p><br /> <br /> <p><br /> The workshop will take place immediately following the [http://conferences.ncl.ac.uk/concur-2012/ CONCUR International Conference] taking place in Newcastle-upon-Tyne<br /> 4-7th September 2012.<br /> </p> <br /> <br /> <hr><br /> <br /> <h3 id="speakers">Invited speakers</h3> <br /> <br /> <ul><br /> <li>[http://cs.famaf.unc.edu.ar/~dargenio/ Pedro D'Argenio], FaMAF, Universidad Nacional de Cordoba<br /> <br><br /> <em>Security analysis in probabilistic distributed protocols via bounded reachability</em><br /> </li><br /> <li>[http://www.dsi.unive.it/~marin/ Andrea Marin], Universita di Venezia<br><br /> <em>Compositional model specifications and analyses via product-forms</em></li><br /> <li>[http://wwwhome.cs.utwente.nl/~vdpol/ Jaco van de Pol], University of Twente<br /> <br><br /> <em>Symbolic manipulation of markov automata</em><br /> </li><br /> <li>[http://www.pst.ifi.lmu.de/people/staff/tribastone/ Mirco Tribastone], Ludwig-Maximilians-Universit&#228;t M&#252;nchen <br /> <br><br /> <em>Exact aggregation for fluid process algebra models</em><br /> </li><br /> </ul><br /> <br /> <p><br /> Abstracts of the invited talks are available [[#abstractsX|here]].<br /> </p><br /> <br /> <hr><br /> <br /> <h3 id="registration">Registration</h3><br /> <br /> <p><br /> Registration will be at a cost of £25. Registration is free for members of SICSA institutions.<br><br /> Registration is available through the [http://www.epay.ed.ac.uk/browse/extra_info.asp?compid=1&catid=42&modid=2&prodid=795&deptid=24&prodvarid=0 online registration system].<br /> </p><br /> <br /> <hr><br /> <br /> <h3 id="posters">Posters</h3><br /> <br /> <p><br /> We invited posters under two categories:<br /> </p><br /> <br /> <ul><li><br /> Presentation of recent or on-going work in relation to the themes of MLQA.<br /> </li><br /> <li><br /> Overview of the recent research activities of a research group related to the themes of MLQA.<br /> </li><br /> </ul><br /> <br /> <p><br /> We equally encourage submissions from both research leaders, junior researchers and PhD students.<br /> </p><br /> <br /> <p><br /> Posters should be printed by the <em>participants</em> in their preferred size.<br /> </p><br /> <br /> <p><br /> Notification of your intention to submit, along with a title and short description of the poster, should be sent by <b>August 31</b> to [mailto:gethin.norman@glasgow.ac.uk gethin.norman@glasgow.ac.uk].<br /> </p><br /> <br /> <hr><br /> <br /> <h3 id="programme">Preliminary Programme</h3><br /> <br /> <ul><br /> <li>09:30 - 09:45 <em>Opening</em><br /> </li><br /> <li>09:45 - 10:30 <em>invited talk</em><br /> <br><br><br /> </li><br /> <li>10:30 - 11:00 <em>coffee</em><br /> <br><br><br /> </li><br /> <li>11:00 - 11:45 <em>Invited talk</em><br /> </li><br /> <li>11:45 - 12:30 <em>Invited talk</em><br /> <br><br><br /> </li><br /> <li>12:30 - 14:00 <em>lunch & poster session</em><br /> <br><br><br /> </li><br /> <li>14:00 - 14:30 <em>SICSA Contributed talk</em><br /> </li><br /> <li>14:30 - 15:00 <em>SICSA Contributed talk</em><br /> </li><br /> <li>15:00 - 15:30 <em>SICSA Contributed talk</em><br /> <br><br><br /> </li><br /> <li>15:30 - 16:00 <em>coffee</em><br /> <br><br><br /> </li><br /> <li>16:00 - 17:00 <em>MLQA business meeting</em><br /> </li><br /> </ul><br /> <br /> <hr><br /> <br /> <h3 id="travel">Travel and Accommodation</h3><br /> <br /> <p><br /> The workshop will take place at the<br /> Informatics Forum of the School of Informatics, University of Edinburgh. For details on its location as well as links for travel directions see [http://www.ed.ac.uk/schools-departments/informatics/about/location here]. For those attending CONCUR, Edinburgh is approximately 90 minutes from Newcastle by train.<br /> </p><br /> <br /> <p><br /> For information regarding accommodation will be available soon.<br /> <hr><br /> <br /> <h3 id="organisers">Organisers</h3><br /> <ul><br /> <li>[http://homepages.inf.ed.ac.uk/jeh/ Jane Hilston], University of Edinburgh</li><br /> <li>[http://www.dcs.gla.ac.uk/people/personal/gethin/ Gethin Norman], University of Glasgow</li><br /> </ul><br /> <br /> <hr><br /> <br /> <div id="abstractsX"></div><br /> <h3 id="abstracts">Abstracts of Invited Talks</h3><br /> <br /> <ul><br /> <li>[http://cs.famaf.unc.edu.ar/~dargenio/ Pedro D'Argenio], FaMAF, Universidad Nacional de Cordoba<br /> <br><br /> Title: <em>Security analysis in probabilistic distributed protocols via bounded reachability.<br /> </em><br><br /> Abstract: Probabilistic model checking computes the probability values of a given property quantifying over all possible schedulers (also known as adversaries or policies). It turns out that maximum and minimum probabilities calculated in such a way are overestimations on models of distributed systems in which components are loosely coupled and share little information with each other. The problem exacerbates, if n addition the system is intended to protect private information.<br /> <br><br><br /> In this talk, we will (1) discuss the problem, (2) give a characterization for the set of schedulers that respect the distributed nature of process and the idea of secrecy, (3) report of some important properties of this class of schedulers, and (4) present an algorithm to analyze time-bounded reachability properties based on polynomial optimization. We will briefly discuss a prototype implementation and report some case studies.<br /> <br><br></li><br /> <li>[http://www.dsi.unive.it/~marin/ Andrea Marin], Universita di Venezia<br /> <br><br /> Title: <em>Compositional model specifications and analyses via product-forms</em><br><br /> Abstract: Compositionality is an important aspect of many formalisms used for<br /> quantitative analysis of computer software and hardware architectures<br /> and communication systems. Compositionality allows for the specification <br /> of complex models in terms of cooperations of simpler components in<br /> a modular and hierarchical way. <br /> <br><br><br /> However, these elegant and often compact model definitions often hide<br /> a huge complexity in the structure of the state space. For models with<br /> underlying continuous or discrete time Markov chains this implies that the quantitative<br /> evaluation of performance and reliability indices cannot rely on<br /> brute force approaches (such as the solution of the set of global balance<br /> equations). Therefore, from the point of view of the<br /> quantitative analysis of compositional models, an approach<br /> that allows one to tackle large state spaces is needed. When<br /> the models are characterised by underlying continuous time Markov<br /> chains (e.g., stochastic Petri nets, Performance Evaluation Process algebra -PEPA-) <br /> product-form theory may be successfully applied. Informally, product-forms<br /> aim at studying the model properties in steady-state starting from the<br /> analysis of its isolated components which are opportunely "parametrised" in order<br /> to take into account the interactions with the remaining parts of the model. <br /> <br><br><br /> After introducing product-form theory in stochastic process algebra<br /> domain, the talk will address the problem of deciding if product-form conditions<br /> are satisfied by the composition of a set of components and how the parameterisation<br /> of these components can be achieved. Special attention will be devoted to the<br /> automation of these steps even in cases of models with infinite state spaces.<br /> The Iterative Numerical Algorithm for Product-forms will be presented. <br /> Concluding remarks will consider the problem of the computation of the <br /> normalising constant and product-form approximations.<br /> <br><br><br /> </li><br /> <li>[http://wwwhome.cs.utwente.nl/~vdpol/ Jaco van de Pol], University of Twente<br /> <br><br /> Title: <em>Symbolic Manipulation of Markov Automata</em><br><br /> Abstract: Markov automata combine non-deterministic choice, probabilistic choice,<br /> and stochastic delays, and come with a natural notion of parallel composition.<br /> Since these automata generalize labeled transition systems and both<br /> discrete-time and continuous-time Markov Chains, they provide a rich<br /> model of computation.<br /> <br><br><br /> We will present the process algebra MAPA for specifying Markov Automata<br /> in a symbolic manner. Specifications in MAPA can be very concise, due to<br /> parallel composition and the use of data types. MAPA specifications can<br /> be transformed into a linear process format, which is an excellent basis<br /> for symbolic transformation and optimization of Markov Automata.<br /> <br><br></li> <br /> <li>[http://www.pst.ifi.lmu.de/people/staff/tribastone/ Mirco Tribastone], Ludwig-Maximilians-Universit&#228;t M&#252;nchen <br /> <br><br /> Title: <em>Exact Aggregation for Fluid Process Algebra Models</em><br><br /> Abstract: Recent research in stochastic process algebra has led to efficient fluid approximation techniques obtained by aggregating large populations of sequential components into a single continuous-state variable represented as an ordinary differential equation (ODE). In this talk I will show that, when aggregation is performed higher up in the syntax tree of a model --- i.e., when one is interested in replicas of composite processes --- the resulting ODE system does not scale well with population sizes. I will present two techniques to tackle this problem. The first one is a model-to-model transformation at the process-algebra level. It converts a model with a large ODE system into another one whose size is independent from all population levels, but whose solution is related exactly to that of the original system. Simple syntactic checks are a necessary condition for this transformation to be carried out. The second technique enlarges the class of models amenable to exact aggregation. It performs a transformation directly at the level of the underlying ODE system, which is induced by a novel notion of behavioural equivalence for process algebra with fluid semantics. <br /> </li><br /> </ul><br /> <br /> <br /> <hr><br /> <br /> <div id="minutes"></div><br /> <h3 id="minutess">Minutes</h3><br /> <br /> Minutes of MLQA 2012 is avaliable here.</div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=MLQA_2012&diff=441 MLQA 2012 2012-06-29T01:44:46Z

<p>Ender: </p> <hr /> <div><table width="100%" border="0"><br /> <tr><br /> <td><br /> <h1>Joint Workshop on Compositional Modelling and Analysis of Quantitative Systems</h1><br /> <b>September 8, 2012</b><br /> <b>University of Edinburgh</b><br /> </td><br /> <td>&nbsp;</td><br /> <td align="right"><br /> <table width="100%" border="0"><br /> <tr><br /> <td align="right"><br />  </td><br /> </tr></table><br /> [[File:Sicsa.jpg|link=http://www.sicsa.ac.uk/themes/modelling-and-abstraction]]<br /> </td><br /> </tr><br /> </table><br /> <br /> __TOC__<br /> <br /> <hr><br /> <br /> <h3 id="overview">Overview</h3><br /> <br /> <p><br /> The workshop combines the Fourth annual meeting of the [http://wiki.ercim.eu/wg/MLQA ERCIM Working Group on Models and Logics for Quantitative Analysis (MLQA)] with a [http://www.sicsa.ac.uk/themes/modelling-and-abstraction SICSA Modelling and Abstraction Theme] event.<br /> </p><br /> <br /> <p><br /> The theme of the workshop is <em>Compositional Modelling and Analysis of Quantitative Systems</em>. Compositionality is a key concept in both the modeling and analysis of computer systems. It is only by decomposing large complex system into smaller pieces, we can build and analyse these systems.<br /> </p><br /> <br /> <p><br /> The aim of the workshop is to bring together researchers working on quantitative modelling and analysis of computer systems focusing on research using compositional techniques. The workshop hopes to encourage interaction and collaboration between the attendees in developing compositional approaches. <br /> The workshop will bring together MLQA participants from across Europe with contributors to the SICSA theme of 'Modelling and Abstraction'. However, participation from outside MLQA and the SICSA theme are also welcome. <br /> </p><br /> <br /> <p><br /> The workshop will take place immediately following the [http://conferences.ncl.ac.uk/concur-2012/ CONCUR International Conference] taking place in Newcastle-upon-Tyne<br /> 4-7th September 2012.<br /> </p> <br /> <br /> <hr><br /> <br /> <h3 id="speakers">Invited speakers</h3> <br /> <br /> <ul><br /> <li>[http://cs.famaf.unc.edu.ar/~dargenio/ Pedro D'Argenio], FaMAF, Universidad Nacional de Cordoba<br /> <br><br /> <em>Security analysis in probabilistic distributed protocols via bounded reachability</em><br /> </li><br /> <li>[http://www.dsi.unive.it/~marin/ Andrea Marin], Universita di Venezia<br><br /> <em>Compositional model specifications and analyses via product-forms</em></li><br /> <li>[http://wwwhome.cs.utwente.nl/~vdpol/ Jaco van de Pol], University of Twente<br /> <br><br /> <em>Symbolic manipulation of markov automata</em><br /> </li><br /> <li>[http://www.pst.ifi.lmu.de/people/staff/tribastone/ Mirco Tribastone], Ludwig-Maximilians-Universit&#228;t M&#252;nchen <br /> <br><br /> <em>Exact aggregation for fluid process algebra models</em><br /> </li><br /> </ul><br /> <br /> <p><br /> Abstracts of the invited talks are available [[#abstractsX|here]].<br /> </p><br /> <br /> <hr><br /> <br /> <h3 id="registration">Registration</h3><br /> <br /> <p><br /> Registration will be at a cost of £25. Registration is free for members of SICSA institutions.<br><br /> Registration is available through the [http://www.epay.ed.ac.uk/browse/extra_info.asp?compid=1&catid=42&modid=2&prodid=795&deptid=24&prodvarid=0 online registration system].<br /> </p><br /> <br /> <hr><br /> <br /> <h3 id="posters">Posters</h3><br /> <br /> <p><br /> We invited posters under two categories:<br /> </p><br /> <br /> <ul><li><br /> Presentation of recent or on-going work in relation to the themes of MLQA.<br /> </li><br /> <li><br /> Overview of the recent research activities of a research group related to the themes of MLQA.<br /> </li><br /> </ul><br /> <br /> <p><br /> We equally encourage submissions from both research leaders, junior researchers and PhD students.<br /> </p><br /> <br /> <p><br /> Posters should be printed by the <em>participants</em> in their preferred size.<br /> </p><br /> <br /> <p><br /> Notification of your intention to submit, along with a title and short description of the poster, should be sent by <b>August 31</b> to [mailto:gethin.norman@glasgow.ac.uk gethin.norman@glasgow.ac.uk].<br /> </p><br /> <br /> <hr><br /> <br /> <h3 id="programme">Preliminary Programme</h3><br /> <br /> <ul><br /> <li>09:30 - 09:45 <em>Opening</em><br /> </li><br /> <li>09:45 - 10:30 <em>invited talk</em><br /> <br><br><br /> </li><br /> <li>10:30 - 11:00 <em>coffee</em><br /> <br><br><br /> </li><br /> <li>11:00 - 11:45 <em>Invited talk</em><br /> </li><br /> <li>11:45 - 12:30 <em>Invited talk</em><br /> <br><br><br /> </li><br /> <li>12:30 - 14:00 <em>lunch & poster session</em><br /> <br><br><br /> </li><br /> <li>14:00 - 14:30 <em>SICSA Contributed talk</em><br /> </li><br /> <li>14:30 - 15:00 <em>SICSA Contributed talk</em><br /> </li><br /> <li>15:00 - 15:30 <em>SICSA Contributed talk</em><br /> <br><br><br /> </li><br /> <li>15:30 - 16:00 <em>coffee</em><br /> <br><br><br /> </li><br /> <li>16:00 - 17:00 <em>MLQA business meeting</em><br /> </li><br /> </ul><br /> <br /> <hr><br /> <br /> <h3 id="travel">Travel and Accommodation</h3><br /> <br /> <p><br /> The workshop will take place at the<br /> Informatics Forum of the School of Informatics, University of Edinburgh. For details on its location as well as links for travel directions see [http://www.ed.ac.uk/schools-departments/informatics/about/location here]. For those attending CONCUR, Edinburgh is approximately 90 minutes from Newcastle by train.<br /> </p><br /> <br /> <p><br /> For information regarding accommodation will be available soon.<br /> <hr><br /> <br /> <h3 id="organisers">Organisers</h3><br /> <ul><br /> <li>[http://homepages.inf.ed.ac.uk/jeh/ Jane Hilston], University of Edinburgh</li><br /> <li>[http://www.dcs.gla.ac.uk/people/personal/gethin/ Gethin Norman], University of Glasgow</li><br /> </ul><br /> <br /> <hr><br /> <br /> <div id="abstractsX"></div><br /> <h3 id="abstracts">Abstracts of Invited Talks</h3><br /> <br /> <ul><br /> <li>[http://cs.famaf.unc.edu.ar/~dargenio/ Pedro D'Argenio], FaMAF, Universidad Nacional de Cordoba<br /> <br><br /> Title: <em>Security analysis in probabilistic distributed protocols via bounded reachability.<br /> </em><br><br /> Abstract: Probabilistic model checking computes the probability values of a given property quantifying over all possible schedulers (also known as adversaries or policies). It turns out that maximum and minimum probabilities calculated in such a way are overestimations on models of distributed systems in which components are loosely coupled and share little information with each other. The problem exacerbates, if n addition the system is intended to protect private information.<br /> <br><br><br /> In this talk, we will (1) discuss the problem, (2) give a characterization for the set of schedulers that respect the distributed nature of process and the idea of secrecy, (3) report of some important properties of this class of schedulers, and (4) present an algorithm to analyze time-bounded reachability properties based on polynomial optimization. We will briefly discuss a prototype implementation and report some case studies.<br /> <br><br></li><br /> <li>[http://www.dsi.unive.it/~marin/ Andrea Marin], Universita di Venezia<br /> <br><br /> Title: <em>Compositional model specifications and analyses via product-forms</em><br><br /> Abstract: Compositionality is an important aspect of many formalisms used for<br /> quantitative analysis of computer software and hardware architectures<br /> and communication systems. Compositionality allows for the specification <br /> of complex models in terms of cooperations of simpler components in<br /> a modular and hierarchical way. <br /> <br><br><br /> However, these elegant and often compact model definitions often hide<br /> a huge complexity in the structure of the state space. For models with<br /> underlying continuous or discrete time Markov chains this implies that the quantitative<br /> evaluation of performance and reliability indices cannot rely on<br /> brute force approaches (such as the solution of the set of global balance<br /> equations). Therefore, from the point of view of the<br /> quantitative analysis of compositional models, an approach<br /> that allows one to tackle large state spaces is needed. When<br /> the models are characterised by underlying continuous time Markov<br /> chains (e.g., stochastic Petri nets, Performance Evaluation Process algebra -PEPA-) <br /> product-form theory may be successfully applied. Informally, product-forms<br /> aim at studying the model properties in steady-state starting from the<br /> analysis of its isolated components which are opportunely "parametrised" in order<br /> to take into account the interactions with the remaining parts of the model. <br /> <br><br><br /> After introducing product-form theory in stochastic process algebra<br /> domain, the talk will address the problem of deciding if product-form conditions<br /> are satisfied by the composition of a set of components and how the parameterisation<br /> of these components can be achieved. Special attention will be devoted to the<br /> automation of these steps even in cases of models with infinite state spaces.<br /> The Iterative Numerical Algorithm for Product-forms will be presented. <br /> Concluding remarks will consider the problem of the computation of the <br /> normalising constant and product-form approximations.<br /> <br><br><br /> </li><br /> <li>[http://wwwhome.cs.utwente.nl/~vdpol/ Jaco van de Pol], University of Twente<br /> <br><br /> Title: <em>Symbolic Manipulation of Markov Automata</em><br><br /> Abstract: Markov automata combine non-deterministic choice, probabilistic choice,<br /> and stochastic delays, and come with a natural notion of parallel composition.<br /> Since these automata generalize labeled transition systems and both<br /> discrete-time and continuous-time Markov Chains, they provide a rich<br /> model of computation.<br /> <br><br><br /> We will present the process algebra MAPA for specifying Markov Automata<br /> in a symbolic manner. Specifications in MAPA can be very concise, due to<br /> parallel composition and the use of data types. MAPA specifications can<br /> be transformed into a linear process format, which is an excellent basis<br /> for symbolic transformation and optimization of Markov Automata.<br /> <br><br></li> <br /> <li>[http://www.pst.ifi.lmu.de/people/staff/tribastone/ Mirco Tribastone], Ludwig-Maximilians-Universit&#228;t M&#252;nchen <br /> <br><br /> Title: <em>Exact Aggregation for Fluid Process Algebra Models</em><br><br /> Abstract: Recent research in stochastic process algebra has led to efficient fluid approximation techniques obtained by aggregating large populations of sequential components into a single continuous-state variable represented as an ordinary differential equation (ODE). In this talk I will show that, when aggregation is performed higher up in the syntax tree of a model --- i.e., when one is interested in replicas of composite processes --- the resulting ODE system does not scale well with population sizes. I will present two techniques to tackle this problem. The first one is a model-to-model transformation at the process-algebra level. It converts a model with a large ODE system into another one whose size is independent from all population levels, but whose solution is related exactly to that of the original system. Simple syntactic checks are a necessary condition for this transformation to be carried out. The second technique enlarges the class of models amenable to exact aggregation. It performs a transformation directly at the level of the underlying ODE system, which is induced by a novel notion of behavioural equivalence for process algebra with fluid semantics. <br /> </li><br /> </ul></div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=MLQA_2012&diff=440 MLQA 2012 2012-06-29T01:44:17Z

<p>Ender: </p> <hr /> <div><table width="100%" border="0"><br /> <tr><br /> <td><br /> <h1>Joint Workshop on Compositional Modelling and Analysis of Quantitative Systems</h1><br /> <b>September 8, 2012</b><br /> <b>University of Edinburgh</b><br /> </td><br /> <td>&nbsp;</td><br /> <td align="right"><br /> <table width="100%" border="0"><br /> <tr><br /> <td align="right"><br />  </td><br /> </tr></table><br /> [[File:Sicsa.jpg|link=http://www.sicsa.ac.uk/themes/modelling-and-abstraction]]<br /> </td><br /> </tr><br /> </table><br /> <br /> __TOC__<br /> <br /> <hr><br /> <br /> <h3 id="overview">Overview</h3><br /> <br /> <p><br /> The workshop combines the Fourth annual meeting of the [http://wiki.ercim.eu/wg/MLQA ERCIM Working Group on Models and Logics for Quantitative Analysis (MLQA)] with a [http://www.sicsa.ac.uk/themes/modelling-and-abstraction SICSA Modelling and Abstraction Theme] event.<br /> </p><br /> <br /> <p><br /> The theme of the workshop is <em>Compositional Modelling and Analysis of Quantitative Systems</em>. Compositionality is a key concept in both the modeling and analysis of computer systems. It is only by decomposing large complex system into smaller pieces, we can build and analyse these systems.<br /> </p><br /> <br /> <p><br /> The aim of the workshop is to bring together researchers working on quantitative modelling and analysis of computer systems focusing on research using compositional techniques. The workshop hopes to encourage interaction and collaboration between the attendees in developing compositional approaches. <br /> The workshop will bring together MLQA participants from across Europe with contributors to the SICSA theme of 'Modelling and Abstraction'. However, participation from outside MLQA and the SICSA theme are also welcome. <br /> </p><br /> <br /> <p><br /> The workshop will take place immediately following the [http://conferences.ncl.ac.uk/concur-2012/ CONCUR International Conference] taking place in Newcastle-upon-Tyne<br /> 4-7th September 2012.<br /> </p> <br /> <br /> <hr><br /> <br /> <h3 id="speakers">Invited speakers</h3> <br /> <br /> <ul><br /> <li>[http://cs.famaf.unc.edu.ar/~dargenio/ Pedro D'Argenio], FaMAF, Universidad Nacional de Cordoba<br /> <br><br /> <em>Security analysis in probabilistic distributed protocols via bounded reachability</em><br /> </li><br /> <li>[http://www.dsi.unive.it/~marin/ Andrea Marin], Universita di Venezia<br><br /> <em>Compositional model specifications and analyses via product-forms</em></li><br /> <li>[http://wwwhome.cs.utwente.nl/~vdpol/ Jaco van de Pol], University of Twente<br /> <br><br /> <em>Symbolic manipulation of markov automata</em><br /> </li><br /> <li>[http://www.pst.ifi.lmu.de/people/staff/tribastone/ Mirco Tribastone], Ludwig-Maximilians-Universit&#228;t M&#252;nchen <br /> <br><br /> <em>Exact aggregation for fluid process algebra models</em><br /> </li><br /> </ul><br /> <br /> <p><br /> Abstracts of the invited talks are available [[#abstractsX|here]].<br /> </p><br /> <br /> <hr><br /> <br /> <h3 id="registration">Registration</h3><br /> <br /> <p><br /> Registration will be at a cost of £25. Registration is free for members of SICSA institutions.<br><br /> Registration is available through the [http://www.epay.ed.ac.uk/browse/extra_info.asp?compid=1&catid=42&modid=2&prodid=795&deptid=24&prodvarid=0 online registration system].<br /> </p><br /> <br /> <hr><br /> <br /> <h3 id="posters">Posters</h3><br /> <br /> <br /> <p><br /> We invited posters under two categories:<br /> </p><br /> <br /> <ul><li><br /> Presentation of recent or on-going work in relation to the themes of MLQA.<br /> </li><br /> <li><br /> Overview of the recent research activities of a research group related to the themes of MLQA.<br /> </li><br /> </ul><br /> <br /> <p><br /> We equally encourage submissions from both research leaders, junior researchers and PhD students.<br /> </p><br /> <br /> <p><br /> Posters should be printed by the <em>participants</em> in their preferred size.<br /> </p><br /> <br /> <p><br /> Notification of your intention to submit, along with a title and short description of the poster, should be sent by <b>August 31</b> to [mailto:gethin.norman@glasgow.ac.uk gethin.norman@glasgow.ac.uk].<br /> </p><br /> <br /> <hr><br /> <br /> <h3 id="programme">Preliminary Programme</h3><br /> <br /> <ul><br /> <li>09:30 - 09:45 <em>Opening</em><br /> </li><br /> <li>09:45 - 10:30 <em>invited talk</em><br /> <br><br><br /> </li><br /> <li>10:30 - 11:00 <em>coffee</em><br /> <br><br><br /> </li><br /> <li>11:00 - 11:45 <em>Invited talk</em><br /> </li><br /> <li>11:45 - 12:30 <em>Invited talk</em><br /> <br><br><br /> </li><br /> <li>12:30 - 14:00 <em>lunch & poster session</em><br /> <br><br><br /> </li><br /> <li>14:00 - 14:30 <em>SICSA Contributed talk</em><br /> </li><br /> <li>14:30 - 15:00 <em>SICSA Contributed talk</em><br /> </li><br /> <li>15:00 - 15:30 <em>SICSA Contributed talk</em><br /> <br><br><br /> </li><br /> <li>15:30 - 16:00 <em>coffee</em><br /> <br><br><br /> </li><br /> <li>16:00 - 17:00 <em>MLQA business meeting</em><br /> </li><br /> </ul><br /> <br /> <hr><br /> <br /> <h3 id="travel">Travel and Accommodation</h3><br /> <br /> <p><br /> The workshop will take place at the<br /> Informatics Forum of the School of Informatics, University of Edinburgh. For details on its location as well as links for travel directions see [http://www.ed.ac.uk/schools-departments/informatics/about/location here]. For those attending CONCUR, Edinburgh is approximately 90 minutes from Newcastle by train.<br /> </p><br /> <br /> <p><br /> For information regarding accommodation will be available soon.<br /> <hr><br /> <br /> <h3 id="organisers">Organisers</h3><br /> <ul><br /> <li>[http://homepages.inf.ed.ac.uk/jeh/ Jane Hilston], University of Edinburgh</li><br /> <li>[http://www.dcs.gla.ac.uk/people/personal/gethin/ Gethin Norman], University of Glasgow</li><br /> </ul><br /> <br /> <hr><br /> <br /> <div id="abstractsX"></div><br /> <h3 id="abstracts">Abstracts of Invited Talks</h3><br /> <br /> <ul><br /> <li>[http://cs.famaf.unc.edu.ar/~dargenio/ Pedro D'Argenio], FaMAF, Universidad Nacional de Cordoba<br /> <br><br /> Title: <em>Security analysis in probabilistic distributed protocols via bounded reachability.<br /> </em><br><br /> Abstract: Probabilistic model checking computes the probability values of a given property quantifying over all possible schedulers (also known as adversaries or policies). It turns out that maximum and minimum probabilities calculated in such a way are overestimations on models of distributed systems in which components are loosely coupled and share little information with each other. The problem exacerbates, if n addition the system is intended to protect private information.<br /> <br><br><br /> In this talk, we will (1) discuss the problem, (2) give a characterization for the set of schedulers that respect the distributed nature of process and the idea of secrecy, (3) report of some important properties of this class of schedulers, and (4) present an algorithm to analyze time-bounded reachability properties based on polynomial optimization. We will briefly discuss a prototype implementation and report some case studies.<br /> <br><br></li><br /> <li>[http://www.dsi.unive.it/~marin/ Andrea Marin], Universita di Venezia<br /> <br><br /> Title: <em>Compositional model specifications and analyses via product-forms</em><br><br /> Abstract: Compositionality is an important aspect of many formalisms used for<br /> quantitative analysis of computer software and hardware architectures<br /> and communication systems. Compositionality allows for the specification <br /> of complex models in terms of cooperations of simpler components in<br /> a modular and hierarchical way. <br /> <br><br><br /> However, these elegant and often compact model definitions often hide<br /> a huge complexity in the structure of the state space. For models with<br /> underlying continuous or discrete time Markov chains this implies that the quantitative<br /> evaluation of performance and reliability indices cannot rely on<br /> brute force approaches (such as the solution of the set of global balance<br /> equations). Therefore, from the point of view of the<br /> quantitative analysis of compositional models, an approach<br /> that allows one to tackle large state spaces is needed. When<br /> the models are characterised by underlying continuous time Markov<br /> chains (e.g., stochastic Petri nets, Performance Evaluation Process algebra -PEPA-) <br /> product-form theory may be successfully applied. Informally, product-forms<br /> aim at studying the model properties in steady-state starting from the<br /> analysis of its isolated components which are opportunely "parametrised" in order<br /> to take into account the interactions with the remaining parts of the model. <br /> <br><br><br /> After introducing product-form theory in stochastic process algebra<br /> domain, the talk will address the problem of deciding if product-form conditions<br /> are satisfied by the composition of a set of components and how the parameterisation<br /> of these components can be achieved. Special attention will be devoted to the<br /> automation of these steps even in cases of models with infinite state spaces.<br /> The Iterative Numerical Algorithm for Product-forms will be presented. <br /> Concluding remarks will consider the problem of the computation of the <br /> normalising constant and product-form approximations.<br /> <br><br><br /> </li><br /> <li>[http://wwwhome.cs.utwente.nl/~vdpol/ Jaco van de Pol], University of Twente<br /> <br><br /> Title: <em>Symbolic Manipulation of Markov Automata</em><br><br /> Abstract: Markov automata combine non-deterministic choice, probabilistic choice,<br /> and stochastic delays, and come with a natural notion of parallel composition.<br /> Since these automata generalize labeled transition systems and both<br /> discrete-time and continuous-time Markov Chains, they provide a rich<br /> model of computation.<br /> <br><br><br /> We will present the process algebra MAPA for specifying Markov Automata<br /> in a symbolic manner. Specifications in MAPA can be very concise, due to<br /> parallel composition and the use of data types. MAPA specifications can<br /> be transformed into a linear process format, which is an excellent basis<br /> for symbolic transformation and optimization of Markov Automata.<br /> <br><br></li> <br /> <li>[http://www.pst.ifi.lmu.de/people/staff/tribastone/ Mirco Tribastone], Ludwig-Maximilians-Universit&#228;t M&#252;nchen <br /> <br><br /> Title: <em>Exact Aggregation for Fluid Process Algebra Models</em><br><br /> Abstract: Recent research in stochastic process algebra has led to efficient fluid approximation techniques obtained by aggregating large populations of sequential components into a single continuous-state variable represented as an ordinary differential equation (ODE). In this talk I will show that, when aggregation is performed higher up in the syntax tree of a model --- i.e., when one is interested in replicas of composite processes --- the resulting ODE system does not scale well with population sizes. I will present two techniques to tackle this problem. The first one is a model-to-model transformation at the process-algebra level. It converts a model with a large ODE system into another one whose size is independent from all population levels, but whose solution is related exactly to that of the original system. Simple syntactic checks are a necessary condition for this transformation to be carried out. The second technique enlarges the class of models amenable to exact aggregation. It performs a transformation directly at the level of the underlying ODE system, which is induced by a novel notion of behavioural equivalence for process algebra with fluid semantics. <br /> </li><br /> </ul></div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=MLQA_2012&diff=439 MLQA 2012 2012-06-29T01:36:49Z

<p>Ender: </p> <hr /> <div><table width="100%" border="0"><br /> <tr><br /> <td><br /> <h1>Joint Workshop on Compositional Modelling and Analysis of Quantitative Systems</h1><br /> <b>September 8, 2012</b><br /> <b>University of Edinburgh</b><br /> </td><br /> <td>&nbsp;</td><br /> <td align="right"><br /> <table width="100%" border="0"><br /> <tr><br /> <td align="right"><br />  </td><br /> </tr></table><br /> [[File:Sicsa.jpg|link=http://www.sicsa.ac.uk/themes/modelling-and-abstraction]]<br /> </td><br /> </tr><br /> </table><br /> <br /> __TOC__<br /> <br /> <hr><br /> <br /> <h3 id="overview">Overview</h3><br /> <br /> <p><br /> The workshop combines the Fourth annual meeting of the [http://wiki.ercim.eu/wg/MLQA ERCIM Working Group on Models and Logics for Quantitative Analysis (MLQA)] with a [http://www.sicsa.ac.uk/themes/modelling-and-abstraction SICSA Modelling and Abstraction Theme] event.<br /> </p><br /> <br /> <p><br /> The theme of the workshop is <em>Compositional Modelling and Analysis of Quantitative Systems</em>. Compositionality is a key concept in both the modeling and analysis of computer systems. It is only by decomposing large complex system into smaller pieces, we can build and analyse these systems.<br /> </p><br /> <br /> <p><br /> The aim of the workshop is to bring together researchers working on quantitative modelling and analysis of computer systems focusing on research using compositional techniques. The workshop hopes to encourage interaction and collaboration between the attendees in developing compositional approaches. <br /> The workshop will bring together MLQA participants from across Europe with contributors to the SICSA theme of 'Modelling and Abstraction'. However, participation from outside MLQA and the SICSA theme are also welcome. <br /> </p><br /> <br /> <p><br /> The workshop will take place immediately following the [http://conferences.ncl.ac.uk/concur-2012/ CONCUR International Conference] taking place in Newcastle-upon-Tyne<br /> 4-7th September 2012.<br /> </p> <br /> <br /> <hr><br /> <br /> <h3 id="speakers">Invited speakers</h3> <br /> <br /> <ul><br /> <li>[http://cs.famaf.unc.edu.ar/~dargenio/ Pedro D'Argenio], FaMAF, Universidad Nacional de Cordoba<br /> <br><br /> <em>Security analysis in probabilistic distributed protocols via bounded reachability</em><br /> </li><br /> <li>[http://www.dsi.unive.it/~marin/ Andrea Marin], Universita di Venezia<br><br /> <em>Compositional model specifications and analyses via product-forms</em></li><br /> <li>[http://wwwhome.cs.utwente.nl/~vdpol/ Jaco van de Pol], University of Twente<br /> <br><br /> <em>Symbolic manipulation of markov automata</em><br /> </li><br /> <li>[http://www.pst.ifi.lmu.de/people/staff/tribastone/ Mirco Tribastone], Ludwig-Maximilians-Universit&#228;t M&#252;nchen <br /> <br><br /> <em>Exact aggregation for fluid process algebra models</em><br /> </li><br /> </ul><br /> <br /> <p><br /> Abstracts of the invited talks are available [[#abstractsX|here]].<br /> </p><br /> <br /> <hr><br /> <br /> <h3 id="registration">Registration</h3><br /> <br /> <p><br /> Registration will be at a cost of £25. Registration is free for members of SICSA institutions.<br><br /> Please use the [http://www.epay.ed.ac.uk/browse/extra_info.asp?compid=1&catid=42&modid=2&prodid=795&deptid=24&prodvarid=0 online registration system].<br /> </p><br /> <br /> <hr><br /> <br /> <h3 id="posters">Posters</h3><br /> <br /> <br /> <p><br /> We invited posters under two categories:<br /> </p><br /> <br /> <ul><li><br /> Presentation of recent or on-going work in relation to the themes of MLQA.<br /> </li><br /> <li><br /> Overview of the recent research activities of a research group related to the themes of MLQA.<br /> </li><br /> </ul><br /> <br /> <p><br /> We equally encourage submissions from both research leaders, junior researchers and PhD students.<br /> </p><br /> <br /> <p><br /> Posters should be printed by the <em>participants</em> in their preferred size.<br /> </p><br /> <br /> <p><br /> Notification of your intention to submit, along with a title and short description of the poster, should be sent by <b>August 31</b> to [mailto:gethin.norman@glasgow.ac.uk gethin.norman@glasgow.ac.uk].<br /> </p><br /> <br /> <hr><br /> <br /> <h3 id="programme">Preliminary Programme</h3><br /> <br /> <ul><br /> <li>09:30 - 09:45 <em>Opening</em><br /> </li><br /> <li>09:45 - 10:30 <em>invited talk</em><br /> <br><br><br /> </li><br /> <li>10:30 - 11:00 <em>coffee</em><br /> <br><br><br /> </li><br /> <li>11:00 - 11:45 <em>Invited talk</em><br /> </li><br /> <li>11:45 - 12:30 <em>Invited talk</em><br /> <br><br><br /> </li><br /> <li>12:30 - 14:00 <em>lunch & poster session</em><br /> <br><br><br /> </li><br /> <li>14:00 - 14:30 <em>SICSA Contributed talk</em><br /> </li><br /> <li>14:30 - 15:00 <em>SICSA Contributed talk</em><br /> </li><br /> <li>15:00 - 15:30 <em>SICSA Contributed talk</em><br /> <br><br><br /> </li><br /> <li>15:30 - 16:00 <em>coffee</em><br /> <br><br><br /> </li><br /> <li>16:00 - 17:00 <em>MLQA business meeting</em><br /> </li><br /> </ul><br /> <br /> <hr><br /> <br /> <h3 id="travel">Travel and Accommodation</h3><br /> <br /> <p><br /> The workshop will take place at the<br /> Informatics Forum of the School of Informatics, University of Edinburgh. For details on its location as well as links for travel directions see [http://www.ed.ac.uk/schools-departments/informatics/about/location here]. For those attending CONCUR, Edinburgh is approximately 90 minutes from Newcastle by train.<br /> </p><br /> <br /> <p><br /> For information regarding accommodation will be available soon.<br /> <hr><br /> <br /> <h3 id="organisers">Organisers</h3><br /> <ul><br /> <li>[http://homepages.inf.ed.ac.uk/jeh/ Jane Hilston], University of Edinburgh</li><br /> <li>[http://www.dcs.gla.ac.uk/people/personal/gethin/ Gethin Norman], University of Glasgow</li><br /> </ul><br /> <br /> <hr><br /> <br /> <div id="abstractsX"></div><br /> <h3 id="abstracts">Abstracts of Invited Talks</h3><br /> <br /> <ul><br /> <li>[http://cs.famaf.unc.edu.ar/~dargenio/ Pedro D'Argenio], FaMAF, Universidad Nacional de Cordoba<br /> <br><br /> Title: <em>Security analysis in probabilistic distributed protocols via bounded reachability.<br /> </em><br><br /> Abstract: Probabilistic model checking computes the probability values of a given property quantifying over all possible schedulers (also known as adversaries or policies). It turns out that maximum and minimum probabilities calculated in such a way are overestimations on models of distributed systems in which components are loosely coupled and share little information with each other. The problem exacerbates, if n addition the system is intended to protect private information.<br /> <br><br><br /> In this talk, we will (1) discuss the problem, (2) give a characterization for the set of schedulers that respect the distributed nature of process and the idea of secrecy, (3) report of some important properties of this class of schedulers, and (4) present an algorithm to analyze time-bounded reachability properties based on polynomial optimization. We will briefly discuss a prototype implementation and report some case studies.<br /> <br><br></li><br /> <li>[http://www.dsi.unive.it/~marin/ Andrea Marin], Universita di Venezia<br /> <br><br /> Title: <em>Compositional model specifications and analyses via product-forms</em><br><br /> Abstract: Compositionality is an important aspect of many formalisms used for<br /> quantitative analysis of computer software and hardware architectures<br /> and communication systems. Compositionality allows for the specification <br /> of complex models in terms of cooperations of simpler components in<br /> a modular and hierarchical way. <br /> <br><br><br /> However, these elegant and often compact model definitions often hide<br /> a huge complexity in the structure of the state space. For models with<br /> underlying continuous or discrete time Markov chains this implies that the quantitative<br /> evaluation of performance and reliability indices cannot rely on<br /> brute force approaches (such as the solution of the set of global balance<br /> equations). Therefore, from the point of view of the<br /> quantitative analysis of compositional models, an approach<br /> that allows one to tackle large state spaces is needed. When<br /> the models are characterised by underlying continuous time Markov<br /> chains (e.g., stochastic Petri nets, Performance Evaluation Process algebra -PEPA-) <br /> product-form theory may be successfully applied. Informally, product-forms<br /> aim at studying the model properties in steady-state starting from the<br /> analysis of its isolated components which are opportunely "parametrised" in order<br /> to take into account the interactions with the remaining parts of the model. <br /> <br><br><br /> After introducing product-form theory in stochastic process algebra<br /> domain, the talk will address the problem of deciding if product-form conditions<br /> are satisfied by the composition of a set of components and how the parameterisation<br /> of these components can be achieved. Special attention will be devoted to the<br /> automation of these steps even in cases of models with infinite state spaces.<br /> The Iterative Numerical Algorithm for Product-forms will be presented. <br /> Concluding remarks will consider the problem of the computation of the <br /> normalising constant and product-form approximations.<br /> <br><br><br /> </li><br /> <li>[http://wwwhome.cs.utwente.nl/~vdpol/ Jaco van de Pol], University of Twente<br /> <br><br /> Title: <em>Symbolic Manipulation of Markov Automata</em><br><br /> Abstract: Markov automata combine non-deterministic choice, probabilistic choice,<br /> and stochastic delays, and come with a natural notion of parallel composition.<br /> Since these automata generalize labeled transition systems and both<br /> discrete-time and continuous-time Markov Chains, they provide a rich<br /> model of computation.<br /> <br><br><br /> We will present the process algebra MAPA for specifying Markov Automata<br /> in a symbolic manner. Specifications in MAPA can be very concise, due to<br /> parallel composition and the use of data types. MAPA specifications can<br /> be transformed into a linear process format, which is an excellent basis<br /> for symbolic transformation and optimization of Markov Automata.<br /> <br><br></li> <br /> <li>[http://www.pst.ifi.lmu.de/people/staff/tribastone/ Mirco Tribastone], Ludwig-Maximilians-Universit&#228;t M&#252;nchen <br /> <br><br /> Title: <em>Exact Aggregation for Fluid Process Algebra Models</em><br><br /> Abstract: Recent research in stochastic process algebra has led to efficient fluid approximation techniques obtained by aggregating large populations of sequential components into a single continuous-state variable represented as an ordinary differential equation (ODE). In this talk I will show that, when aggregation is performed higher up in the syntax tree of a model --- i.e., when one is interested in replicas of composite processes --- the resulting ODE system does not scale well with population sizes. I will present two techniques to tackle this problem. The first one is a model-to-model transformation at the process-algebra level. It converts a model with a large ODE system into another one whose size is independent from all population levels, but whose solution is related exactly to that of the original system. Simple syntactic checks are a necessary condition for this transformation to be carried out. The second technique enlarges the class of models amenable to exact aggregation. It performs a transformation directly at the level of the underlying ODE system, which is induced by a novel notion of behavioural equivalence for process algebra with fluid semantics. <br /> </li><br /> </ul></div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=MLQA_2012&diff=411 MLQA 2012 2012-06-25T13:26:41Z

<p>Ender: </p> <hr /> <div><table width="100%" border="0"><br /> <tr><br /> <td><br /> <h1>Joint Workshop on Compositional Modelling and Analysis of Quantitative Systems</h1><br /> <b>September 8, 2012</b><br /> <b>University of Edinburgh</b><br /> </td><br /> <td>&nbsp;</td><br /> <td align="right"><br /> <table width="100%" border="0"><br /> <tr><br /> <td align="right"><br />  </td><br /> </tr></table><br /> [[File:Sicsa.jpg|link=http://www.sicsa.ac.uk/themes/modelling-and-abstraction]]<br /> </td><br /> </tr><br /> </table><br /> <br /> __TOC__<br /> <br /> <hr><br /> <br /> <h3 id="overview">Overview</h3><br /> <br /> <p><br /> The workshop combines the Fourth annual meeting of the [http://wiki.ercim.eu/wg/MLQA ERCIM Working Group on Models and Logics for Quantitative Analysis (MLQA)] with a [http://www.sicsa.ac.uk/themes/modelling-and-abstraction SICSA Modelling and Abstraction Theme] event.<br /> </p><br /> <br /> <p><br /> The theme of the workshop is <em>Compositional Modelling and Analysis of Quantitative Systems</em>. Compositionality is a key concept in both the modeling and analysis of computer systems. It is only by decomposing large complex system into smaller pieces, we can build and analyse these systems.<br /> </p><br /> <br /> <p><br /> The aim of the workshop is to bring together researchers working on quantitative modelling and analysis of computer systems focusing on research using compositional techniques. The workshop hopes to encourage interaction and collaboration between the attendees in developing compositional approaches. <br /> The workshop will bring together MLQA participants from across Europe with contributors to the SICSA theme of 'Modelling and Abstraction'. However, participation from outside MLQA and the SICSA theme are also welcome. <br /> </p><br /> <br /> <p><br /> The workshop will take place immediately following the [http://conferences.ncl.ac.uk/concur-2012/ CONCUR International Conference] taking place in Newcastle-upon-Tyne<br /> 4-7th September 2012.<br /> </p> <br /> <br /> <hr><br /> <br /> <h3 id="speakers">Invited speakers</h3> <br /> <br /> <ul><br /> <li>[http://cs.famaf.unc.edu.ar/~dargenio/ Pedro D'Argenio], FaMAF, Universidad Nacional de Cordoba<br /> <br><br /> <em>Security analysis in probabilistic distributed protocols via bounded reachability</em><br /> </li><br /> <li>[http://www.dsi.unive.it/~marin/ Andrea Marin], Universita di Venezia<br><br /> <em>Compositional model specifications and analyses via product-forms</em></li><br /> <li>[http://wwwhome.cs.utwente.nl/~vdpol/ Jaco van de Pol], University of Twente<br /> <br><br /> <em>Symbolic manipulation of markov automata</em><br /> </li><br /> <li>[http://www.pst.ifi.lmu.de/people/staff/tribastone/ Mirco Tribastone], Ludwig-Maximilians-Universit&#228;t M&#252;nchen <br /> <br><br /> <em>Exact aggregation for fluid process algebra models</em><br /> </li><br /> </ul><br /> <br /> <p><br /> Abstracts of the invited talks are available [[#abstractsX|here]].<br /> </p><br /> <br /> <hr><br /> <br /> <h3 id="registration">Registration</h3><br /> <br /> <p><br /> Registration will be at a cost of £25. Registration is free for members of SICSA institutions.<br /> </p><br /> <br /> <hr><br /> <br /> <h3 id="posters">Posters</h3><br /> <br /> <br /> <p><br /> We invited posters under two categories:<br /> </p><br /> <br /> <ul><li><br /> Presentation of recent or on-going work in relation to the themes of MLQA.<br /> </li><br /> <li><br /> Overview of the recent research activities of a research group related to the themes of MLQA.<br /> </li><br /> </ul><br /> <br /> <p><br /> We equally encourage submissions from both research leaders, junior researchers and PhD students.<br /> </p><br /> <br /> <p><br /> Posters should be printed by the <em>participants</em> in their preferred size.<br /> </p><br /> <br /> <p><br /> Notification of your intention to submit, along with a title and short description of the poster, should be sent by <b>August 31</b> to [mailto:gethin.norman@glasgow.ac.uk gethin.norman@glasgow.ac.uk].<br /> </p><br /> <br /> <hr><br /> <br /> <h3 id="programme">Preliminary Programme</h3><br /> <br /> <ul><br /> <li>09:30 - 09:45 <em>Opening</em><br /> </li><br /> <li>09:45 - 10:30 <em>invited talk</em><br /> <br><br><br /> </li><br /> <li>10:30 - 11:00 <em>coffee</em><br /> <br><br><br /> </li><br /> <li>11:00 - 11:45 <em>Invited talk</em><br /> </li><br /> <li>11:45 - 12:30 <em>Invited talk</em><br /> <br><br><br /> </li><br /> <li>12:30 - 14:00 <em>lunch & poster session</em><br /> <br><br><br /> </li><br /> <li>14:00 - 14:30 <em>SICSA Contributed talk</em><br /> </li><br /> <li>14:30 - 15:00 <em>SICSA Contributed talk</em><br /> </li><br /> <li>15:00 - 15:30 <em>SICSA Contributed talk</em><br /> <br><br><br /> </li><br /> <li>15:30 - 16:00 <em>coffee</em><br /> <br><br><br /> </li><br /> <li>16:00 - 17:00 <em>MLQA business meeting</em><br /> </li><br /> </ul><br /> <br /> <hr><br /> <br /> <h3 id="travel">Travel and Accommodation</h3><br /> <br /> <p><br /> The workshop will take place at the<br /> Informatics Forum of the School of Informatics, University of Edinburgh. For details on its location as well as links for travel directions see [http://www.ed.ac.uk/schools-departments/informatics/about/location here]. For those attending CONCUR, Edinburgh is approximately 90 minutes from Newcastle by train.<br /> </p><br /> <br /> <p><br /> For information regarding accommodation will be available soon.<br /> <hr><br /> <br /> <h3 id="organisers">Organisers</h3><br /> <ul><br /> <li>[http://homepages.inf.ed.ac.uk/jeh/ Jane Hilston], University of Edinburgh</li><br /> <li>[http://www.dcs.gla.ac.uk/people/personal/gethin/ Gethin Norman], University of Glasgow</li><br /> </ul><br /> <br /> <hr><br /> <br /> <div id="abstractsX"></div><br /> <h3 id="abstracts">Abstracts of Invited Talks</h3><br /> <br /> <ul><br /> <li>[http://cs.famaf.unc.edu.ar/~dargenio/ Pedro D'Argenio], FaMAF, Universidad Nacional de Cordoba<br /> <br><br /> Title: <em>Security analysis in probabilistic distributed protocols via bounded reachability.<br /> </em><br><br /> Abstract: Probabilistic model checking computes the probability values of a given property quantifying over all possible schedulers (also known as adversaries or policies). It turns out that maximum and minimum probabilities calculated in such a way are overestimations on models of distributed systems in which components are loosely coupled and share little information with each other. The problem exacerbates, if n addition the system is intended to protect private information.<br /> <br><br><br /> In this talk, we will (1) discuss the problem, (2) give a characterization for the set of schedulers that respect the distributed nature of process and the idea of secrecy, (3) report of some important properties of this class of schedulers, and (4) present an algorithm to analyze time-bounded reachability properties based on polynomial optimization. We will briefly discuss a prototype implementation and report some case studies.<br /> <br><br></li><br /> <li>[http://www.dsi.unive.it/~marin/ Andrea Marin], Universita di Venezia<br /> <br><br /> Title: <em>Compositional model specifications and analyses via product-forms</em><br><br /> Abstract: Compositionality is an important aspect of many formalisms used for<br /> quantitative analysis of computer software and hardware architectures<br /> and communication systems. Compositionality allows for the specification <br /> of complex models in terms of cooperations of simpler components in<br /> a modular and hierarchical way. <br /> <br><br><br /> However, these elegant and often compact model definitions often hide<br /> a huge complexity in the structure of the state space. For models with<br /> underlying continuous or discrete time Markov chains this implies that the quantitative<br /> evaluation of performance and reliability indices cannot rely on<br /> brute force approaches (such as the solution of the set of global balance<br /> equations). Therefore, from the point of view of the<br /> quantitative analysis of compositional models, an approach<br /> that allows one to tackle large state spaces is needed. When<br /> the models are characterised by underlying continuous time Markov<br /> chains (e.g., stochastic Petri nets, Performance Evaluation Process algebra -PEPA-) <br /> product-form theory may be successfully applied. Informally, product-forms<br /> aim at studying the model properties in steady-state starting from the<br /> analysis of its isolated components which are opportunely "parametrised" in order<br /> to take into account the interactions with the remaining parts of the model. <br /> <br><br><br /> After introducing product-form theory in stochastic process algebra<br /> domain, the talk will address the problem of deciding if product-form conditions<br /> are satisfied by the composition of a set of components and how the parameterisation<br /> of these components can be achieved. Special attention will be devoted to the<br /> automation of these steps even in cases of models with infinite state spaces.<br /> The Iterative Numerical Algorithm for Product-forms will be presented. <br /> Concluding remarks will consider the problem of the computation of the <br /> normalising constant and product-form approximations.<br /> <br><br><br /> </li><br /> <li>[http://wwwhome.cs.utwente.nl/~vdpol/ Jaco van de Pol], University of Twente<br /> <br><br /> Title: <em>Symbolic Manipulation of Markov Automata</em><br><br /> Abstract: Markov automata combine non-deterministic choice, probabilistic choice,<br /> and stochastic delays, and come with a natural notion of parallel composition.<br /> Since these automata generalize labeled transition systems and both<br /> discrete-time and continuous-time Markov Chains, they provide a rich<br /> model of computation.<br /> <br><br><br /> We will present the process algebra MAPA for specifying Markov Automata<br /> in a symbolic manner. Specifications in MAPA can be very concise, due to<br /> parallel composition and the use of data types. MAPA specifications can<br /> be transformed into a linear process format, which is an excellent basis<br /> for symbolic transformation and optimization of Markov Automata.<br /> <br><br></li> <br /> <li>[http://www.pst.ifi.lmu.de/people/staff/tribastone/ Mirco Tribastone], Ludwig-Maximilians-Universit&#228;t M&#252;nchen <br /> <br><br /> Title: <em>Exact Aggregation for Fluid Process Algebra Models</em><br><br /> Abstract: Recent research in stochastic process algebra has led to efficient fluid approximation techniques obtained by aggregating large populations of sequential components into a single continuous-state variable represented as an ordinary differential equation (ODE). In this talk I will show that, when aggregation is performed higher up in the syntax tree of a model --- i.e., when one is interested in replicas of composite processes --- the resulting ODE system does not scale well with population sizes. I will present two techniques to tackle this problem. The first one is a model-to-model transformation at the process-algebra level. It converts a model with a large ODE system into another one whose size is independent from all population levels, but whose solution is related exactly to that of the original system. Simple syntactic checks are a necessary condition for this transformation to be carried out. The second technique enlarges the class of models amenable to exact aggregation. It performs a transformation directly at the level of the underlying ODE system, which is induced by a novel notion of behavioural equivalence for process algebra with fluid semantics. <br /> </li><br /> </ul></div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=MLQA_2012&diff=410 MLQA 2012 2012-06-25T13:25:58Z

<p>Ender: </p> <hr /> <div><table width="100%" border="0"><br /> <tr><br /> <td><br /> <h1>Joint Workshop on Compositional Modelling and Analysis of Quantitative Systems</h1><br /> <b>September 8, 2012</b><br /> <b>University of Edinburgh</b><br /> </td><br /> <td>&nbsp;</td><br /> <td align="right"><br /> <table width="100%" border="0"><br /> <tr><br /> <td align="right"><br />  </td><br /> </tr></table><br /> [[File:Sicsa.jpg|link=http://www.sicsa.ac.uk/themes/modelling-and-abstraction]]<br /> </td><br /> </tr><br /> </table><br /> <br /> __TOC__<br /> <br /> <hr><br /> <br /> <h3 id="overview">Overview</h3><br /> <br /> <p><br /> The workshop combines the Fourth annual meeting of the [http://wiki.ercim.eu/wg/MLQA ERCIM Working Group on Models and Logics for Quantitative Analysis (MLQA)] with a [http://www.sicsa.ac.uk/themes/modelling-and-abstraction SICSA Modelling and Abstraction Theme] event.<br /> </p><br /> <br /> <p><br /> The theme of the workshop is <em>Compositional Modelling and Analysis of Quantitative Systems</em>. Compositionality is a key concept in both the modeling and analysis of computer systems. It is only by decomposing large complex system into smaller pieces, we can build and analyse these systems.<br /> </p><br /> <br /> <p><br /> The aim of the workshop is to bring together researchers working on quantitative modelling and analysis of computer systems focusing on research using compositional techniques. The workshop hopes to encourage interaction and collaboration between the attendees in developing compositional approaches. <br /> The workshop will bring together MLQA participants from across Europe with contributors to the SICSA theme of 'Modelling and Abstraction'. However, participation from outside MLQA and the SICSA theme are also welcome. <br /> </p><br /> <br /> <p><br /> The workshop will take place immediately following the [http://conferences.ncl.ac.uk/concur-2012/ CONCUR International Conference] taking place in Newcastle-upon-Tyne<br /> 4-7th September 2012.<br /> </p> <br /> <br /> <hr><br /> <br /> <h3 id="speakers">Invited speakers</h3> <br /> <br /> <ul><br /> <li>[http://cs.famaf.unc.edu.ar/~dargenio/ Pedro D'Argenio], FaMAF, Universidad Nacional de Cordoba<br /> <br><br /> <em>Security analysis in probabilistic distributed protocols via bounded reachability</em><br /> </li><br /> <li>[http://www.dsi.unive.it/~marin/ Andrea Marin], Universita di Venezia<br><br /> <em>Compositional model specifications and analyses via product-forms</em></li><br /> <li>[http://wwwhome.cs.utwente.nl/~vdpol/ Jaco van de Pol], University of Twente<br /> <br><br /> <em>Symbolic manipulation of markov automata</em><br /> </li><br /> <li>[http://www.pst.ifi.lmu.de/people/staff/tribastone/ Mirco Tribastone], Ludwig-Maximilians-Universit&#228;t M&#252;nchen <br /> <br><br /> <em>Exact aggregation for fluid process algebra models</em><br /> </li><br /> </ul><br /> <br /> <p><br /> Abstracts of the invited talks are available [[#abstractsX|here]].<br /> </p><br /> <br /> <hr><br /> <br /> <h3 id="registration">Registration</h3><br /> <br /> <p><br /> Registration will be at a cost of £25. Registration is free for members of SICSA institutions.<br /> </p><br /> <br /> <hr><br /> <br /> <h3 id="posters">Posters</h3><br /> <br /> <br /> <p><br /> We invited posters under two categories:<br /> </p><br /> <br /> <ul><li><br /> Presentation of recent or on-going work in relation to the themes of MLQA.<br /> </li><br /> <li><br /> Overview of the recent research activities of a research group related to the themes of MLQA.<br /> </li><br /> </ul><br /> <br /> <p><br /> We equally encourage submissions from both research leaders, junior researchers and PhD students.<br /> </p><br /> <br /> <p><br /> Posters should be printed by the <em>participants</em> in their preferred size.<br /> </p><br /> <br /> <p><br /> Notification of your intention to submit, along with a title and short description of the poster, should be sent by <b>August 31</b> to [mailto:gethin.norman@glasgow.ac.uk gethin.norman@glasgow.ac.uk].<br /> </p><br /> <br /> <hr><br /> <br /> <h3 id="programme">Preliminary Programme</h3><br /> <br /> <ul><br /> <li>09:30 - 09:45 <em>Opening</em><br /> </li><br /> <li>09:45 - 10:30 <em>invited talk</em><br /> <br><br><br /> </li><br /> <li>10:30 - 11:00 <em>coffee</em><br /> <br><br><br /> </li><br /> <li>11:00 - 11:45 <em>Invited talk</em><br /> </li><br /> <li>11:45 - 12:30 <em>Invited talk</em><br /> <br><br><br /> </li><br /> <li>12:30 - 14:00 <em>lunch & poster session</em><br /> <br><br><br /> </li><br /> <li>14:00 - 14:30 <em>SICSA Contributed talk</em><br /> </li><br /> <li>14:30 - 15:00 <em>SICSA Contributed talk</em><br /> </li><br /> <li>15:00 - 15:30 <em>SICSA Contributed talk</em><br /> <br><br><br /> </li><br /> <li>15:30 - 16:00 <em>coffee</em><br /> <br><br><br /> </li><br /> <li>16:00 - 17:00 <em>MLQA business meeting</em><br /> </li><br /> </ul><br /> <br /> <hr><br /> <br /> <h3 id="travel">Travel and Accommodation</h3><br /> <br /> <p><br /> The workshop will take place at the<br /> Informatics Forum of the School of Informatics, University of Edinburgh. For details on its location as well as links for travel directions see [http://www.ed.ac.uk/schools-departments/informatics/about/location here]. For those attending CONCUR, Edinburgh is approximately 90 minutes from Newcastle by train.<br /> </p><br /> <br /> <p><br /> For information regarding accommodation will be available soon.<br /> <hr><br /> <br /> <h3 id="organisers">Organisers</h3><br /> <ul><br /> <li>[http://homepages.inf.ed.ac.uk/jeh/ Jane Hilston], University of Edinburgh</li><br /> <li>[http://www.dcs.gla.ac.uk/people/personal/gethin/ Gethin Norman], University of Glasgow</li><br /> </ul><br /> <br /> <hr><br /> <br /> <div id="abstractsX"></div><br /> <h3 id="abstracts">Abstracts of Invited Talks</h3><br /> <br /> <ul><br /> <li>[http://cs.famaf.unc.edu.ar/~dargenio/ Pedro D'Argenio], FaMAF, Universidad Nacional de Cordoba<br /> <br><br /> Title: <em>Security analysis in probabilistic distributed protocols via bounded reachability.<br /> </em><br><br /> Abstract: Probabilistic model checking computes the probability values of a given property quantifying over all possible schedulers (also known as adversaries or policies). It turns out that maximum and minimum probabilities calculated in such a way are overestimations on models of distributed systems in which components are loosely coupled and share little information with each other. The problem exacerbates, if n addition the system is intended to protect private information.<br /> <br><br><br /> In this talk, we will (1) discuss the problem, (2) give a characterization for the set of schedulers that respect the distributed nature of process and the idea of secrecy, (3) report of some important properties of this class of schedulers, and (4) present an algorithm to analyze time-bounded reachability properties based on polynomial optimization. We will briefly discuss a prototype implementation and report some case studies.<br /> <br><br></li><br /> <li>[http://www.dsi.unive.it/~marin/ Andrea Marin], Universita di Venezia<br /> <br><br /> Title: <em>Compositional model specifications and analyses via product-forms</em><br><br /> Abstract: Compositionality is an important aspect of many formalisms used for<br /> quantitative analysis of computer software and hardware architectures<br /> and communication systems. Compositionality allows for the specification <br /> of complex models in terms of cooperations of simpler components in<br /> a modular and hierarchical way. <br /> However, these elegant and often compact model definitions often hide<br /> a huge complexity in the structure of the state space. For models with<br /> underlying continuous or discrete time Markov chains this implies that the quantitative<br /> evaluation of performance and reliability indices cannot rely on<br /> brute force approaches (such as the solution of the set of global balance<br /> equations). Therefore, from the point of view of the<br /> quantitative analysis of compositional models, an approach<br /> that allows one to tackle large state spaces is needed. When<br /> the models are characterised by underlying continuous time Markov<br /> chains (e.g., stochastic Petri nets, Performance Evaluation Process algebra -PEPA-) <br /> product-form theory may be successfully applied. Informally, product-forms<br /> aim at studying the model properties in steady-state starting from the<br /> analysis of its isolated components which are opportunely "parametrised" in order<br /> to take into account the interactions with the remaining parts of the model. <br /> <br><br><br /> After introducing product-form theory in stochastic process algebra<br /> domain, the talk will address the problem of deciding if product-form conditions<br /> are satisfied by the composition of a set of components and how the parameterisation<br /> of these components can be achieved. Special attention will be devoted to the<br /> automation of these steps even in cases of models with infinite state spaces.<br /> The Iterative Numerical Algorithm for Product-forms will be presented. <br /> Concluding remarks will consider the problem of the computation of the <br /> normalising constant and product-form approximations.<br /> <br><br><br /> </li><br /> <li>[http://wwwhome.cs.utwente.nl/~vdpol/ Jaco van de Pol], University of Twente<br /> <br><br /> Title: <em>Symbolic Manipulation of Markov Automata</em><br><br /> Abstract: Markov automata combine non-deterministic choice, probabilistic choice,<br /> and stochastic delays, and come with a natural notion of parallel composition.<br /> Since these automata generalize labeled transition systems and both<br /> discrete-time and continuous-time Markov Chains, they provide a rich<br /> model of computation.<br /> We will present the process algebra MAPA for specifying Markov Automata<br /> in a symbolic manner. Specifications in MAPA can be very concise, due to<br /> parallel composition and the use of data types. MAPA specifications can<br /> be transformed into a linear process format, which is an excellent basis<br /> for symbolic transformation and optimization of Markov Automata.<br /> </li> <br /> <li>[http://www.pst.ifi.lmu.de/people/staff/tribastone/ Mirco Tribastone], Ludwig-Maximilians-Universit&#228;t M&#252;nchen <br /> <br><br /> Title: <em>Exact Aggregation for Fluid Process Algebra Models</em><br><br /> Abstract: Recent research in stochastic process algebra has led to efficient fluid approximation techniques obtained by aggregating large populations of sequential components into a single continuous-state variable represented as an ordinary differential equation (ODE). In this talk I will show that, when aggregation is performed higher up in the syntax tree of a model --- i.e., when one is interested in replicas of composite processes --- the resulting ODE system does not scale well with population sizes. I will present two techniques to tackle this problem. The first one is a model-to-model transformation at the process-algebra level. It converts a model with a large ODE system into another one whose size is independent from all population levels, but whose solution is related exactly to that of the original system. Simple syntactic checks are a necessary condition for this transformation to be carried out. The second technique enlarges the class of models amenable to exact aggregation. It performs a transformation directly at the level of the underlying ODE system, which is induced by a novel notion of behavioural equivalence for process algebra with fluid semantics. <br /> </li><br /> </ul></div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=MLQA_2012&diff=409 MLQA 2012 2012-06-25T13:22:17Z

<p>Ender: </p> <hr /> <div><table width="100%" border="0"><br /> <tr><br /> <td><br /> <h1>Joint Workshop on Compositional Modelling and Analysis of Quantitative Systems</h1><br /> <b>September 8, 2012</b><br /> <b>University of Edinburgh</b><br /> </td><br /> <td>&nbsp;</td><br /> <td align="right"><br /> <table width="100%" border="0"><br /> <tr><br /> <td align="right"><br />  </td><br /> </tr></table><br /> [[File:Sicsa.jpg|link=http://www.sicsa.ac.uk/themes/modelling-and-abstraction]]<br /> </td><br /> </tr><br /> </table><br /> <br /> __TOC__<br /> <br /> <hr><br /> <br /> <h3 id="overview">Overview</h3><br /> <br /> <p><br /> The workshop combines the Fourth annual meeting of the [http://wiki.ercim.eu/wg/MLQA ERCIM Working Group on Models and Logics for Quantitative Analysis (MLQA)] with a [http://www.sicsa.ac.uk/themes/modelling-and-abstraction SICSA Modelling and Abstraction Theme] event.<br /> </p><br /> <br /> <p><br /> The theme of the workshop is <em>Compositional Modelling and Analysis of Quantitative Systems</em>. Compositionality is a key concept in both the modeling and analysis of computer systems. It is only by decomposing large complex system into smaller pieces, we can build and analyse these systems.<br /> </p><br /> <br /> <p><br /> The aim of the workshop is to bring together researchers working on quantitative modelling and analysis of computer systems focusing on research using compositional techniques. The workshop hopes to encourage interaction and collaboration between the attendees in developing compositional approaches. <br /> The workshop will bring together MLQA participants from across Europe with contributors to the SICSA theme of 'Modelling and Abstraction'. However, participation from outside MLQA and the SICSA theme are also welcome. <br /> </p><br /> <br /> <p><br /> The workshop will take place immediately following the [http://conferences.ncl.ac.uk/concur-2012/ CONCUR International Conference] taking place in Newcastle-upon-Tyne<br /> 4-7th September 2012.<br /> </p> <br /> <br /> <hr><br /> <br /> <h3 id="speakers">Invited speakers</h3> <br /> <br /> <ul><br /> <li>[http://cs.famaf.unc.edu.ar/~dargenio/ Pedro D'Argenio], FaMAF, Universidad Nacional de Cordoba<br /> <br><br /> <em>Security analysis in probabilistic distributed protocols via bounded reachability</em><br /> </li><br /> <li>[http://www.dsi.unive.it/~marin/ Andrea Marin], Universita di Venezia<br><br /> <em>Compositional model specifications and analyses via product-forms</em></li><br /> <li>[http://wwwhome.cs.utwente.nl/~vdpol/ Jaco van de Pol], University of Twente<br /> <br><br /> <em>Symbolic manipulation of markov automata</em><br /> </li><br /> <li>[http://www.pst.ifi.lmu.de/people/staff/tribastone/ Mirco Tribastone], Ludwig-Maximilians-Universit&#228;t M&#252;nchen <br /> <br><br /> <em>Exact aggregation for fluid process algebra models</em><br /> </li><br /> </ul><br /> <br /> <p><br /> Abstracts of the invited talks are available [[#abstractsX|here]].<br /> </p><br /> <br /> <hr><br /> <br /> <h3 id="registration">Registration</h3><br /> <br /> <p><br /> Registration will be at a cost of £25. Registration is free for members of SICSA institutions.<br /> </p><br /> <br /> <hr><br /> <br /> <h3 id="posters">Posters</h3><br /> <br /> <br /> <p><br /> We invited posters under two categories:<br /> </p><br /> <br /> <ul><li><br /> Presentation of recent or on-going work in relation to the themes of MLQA.<br /> </li><br /> <li><br /> Overview of the recent research activities of a research group related to the themes of MLQA.<br /> </li><br /> </ul><br /> <br /> <p><br /> We equally encourage submissions from both research leaders, junior researchers and PhD students.<br /> </p><br /> <br /> <p><br /> Posters should be printed by the <em>participants</em> in their preferred size.<br /> </p><br /> <br /> <p><br /> Notification of your intention to submit, along with a title and short description of the poster, should be sent by <b>August 31</b> to [mailto:gethin.norman@glasgow.ac.uk gethin.norman@glasgow.ac.uk].<br /> </p><br /> <br /> <hr><br /> <br /> <h3 id="programme">Preliminary Programme</h3><br /> <br /> <ul><br /> <li>09:30 - 09:45 <em>Opening</em><br /> </li><br /> <li>09:45 - 10:30 <em>invited talk</em><br /> <br><br><br /> </li><br /> <li>10:30 - 11:00 <em>coffee</em><br /> <br><br><br /> </li><br /> <li>11:00 - 11:45 <em>Invited talk</em><br /> </li><br /> <li>11:45 - 12:30 <em>Invited talk</em><br /> <br><br><br /> </li><br /> <li>12:30 - 14:00 <em>lunch & poster session</em><br /> <br><br><br /> </li><br /> <li>14:00 - 14:30 <em>SICSA Contributed talk</em><br /> </li><br /> <li>14:30 - 15:00 <em>SICSA Contributed talk</em><br /> </li><br /> <li>15:00 - 15:30 <em>SICSA Contributed talk</em><br /> <br><br><br /> </li><br /> <li>15:30 - 16:00 <em>coffee</em><br /> <br><br><br /> </li><br /> <li>16:00 - 17:00 <em>MLQA business meeting</em><br /> </li><br /> </ul><br /> <br /> <hr><br /> <br /> <h3 id="travel">Travel and Accommodation</h3><br /> <br /> <p><br /> The workshop will take place at the<br /> Informatics Forum of the School of Informatics, University of Edinburgh. For details on its location as well as links for travel directions see [http://www.ed.ac.uk/schools-departments/informatics/about/location here]. For those attending CONCUR, Edinburgh is approximately 90 minutes from Newcastle by train.<br /> </p><br /> <br /> <p><br /> For information regarding accommodation will be available soon.<br /> <hr><br /> <br /> <h3 id="organisers">Organisers</h3><br /> <ul><br /> <li>[http://homepages.inf.ed.ac.uk/jeh/ Jane Hilston], University of Edinburgh</li><br /> <li>[http://www.dcs.gla.ac.uk/people/personal/gethin/ Gethin Norman], University of Glasgow</li><br /> </ul><br /> <br /> <hr><br /> <br /> <div id="abstractsX"></div><br /> <h3 id="abstracts">Abstracts of Invited Talks</h3><br /> <br /> <ul><br /> <li>[http://cs.famaf.unc.edu.ar/~dargenio/ Pedro D'Argenio], FaMAF, Universidad Nacional de Cordoba<br /> <br><br /> Title: <em>Security analysis in probabilistic distributed protocols via bounded reachability.<br /> </em><br><br /> Abstract: Probabilistic model checking computes the probability values of a given property quantifying over all possible schedulers (also known as adversaries or policies). It turns out that maximum and minimum probabilities calculated in such a way are overestimations on models of distributed systems in which components are loosely coupled and share little information with each other. The problem exacerbates, if n addition the system is intended to protect private information.<br /> <br><br><br /> In this talk, we will (1) discuss the problem, (2) give a characterization for the set of schedulers that respect the distributed nature of process and the idea of secrecy, (3) report of some important properties of this class of schedulers, and (4) present an algorithm to analyze time-bounded reachability properties based on polynomial optimization. We will briefly discuss a prototype implementation and report some case studies.<br /> <br><br></li><br /> <li>[http://www.dsi.unive.it/~marin/ Andrea Marin], Universita di Venezia<br /> <br><br /> Title: <em>Compositional model specifications and analyses via product-forms</em><br><br /> Abstract: Compositionality is an important aspect of many formalisms used for<br /> quantitative analysis of computer software and hardware architectures<br /> and communication systems. Compositionality allows for the specification <br /> of complex models in terms of cooperations of simpler components in<br /> a modular and hierarchical way. <br /> However, these elegant and often compact model definitions often hide<br /> a huge complexity in the structure of the state space. For models with<br /> underlying continuous or discrete time Markov chains this implies that the quantitative<br /> evaluation of performance and reliability indices cannot rely on<br /> brute force approaches (such as the solution of the set of global balance<br /> equations). Therefore, from the point of view of the<br /> quantitative analysis of compositional models, an approach<br /> that allows one to tackle large state spaces is needed. When<br /> the models are characterised by underlying continuous time Markov<br /> chains (e.g., stochastic Petri nets, Performance Evaluation Process algebra -PEPA-) <br /> product-form theory may be successfully applied. Informally, product-forms<br /> aim at studying the model properties in steady-state starting from the<br /> analysis of its isolated components which are opportunely "parametrised" in order<br /> to take into account the interactions with the remaining parts of the model. <br /> <br><br><br /> After introducing product-form theory in stochastic process algebra<br /> domain, the talk will address the problem of deciding if product-form conditions<br /> are satisfied by the composition of a set of components and how the parameterisation<br /> of these components can be achieved. Special attention will be devoted to the<br /> automation of these steps even in cases of models with infinite state spaces.<br /> The Iterative Numerical Algorithm for Product-forms will be presented. <br /> Concluding remarks will consider the problem of the computation of the <br /> normalising constant and product-form approximations.<br /> <br><br><br /> </li><br /> <br /> <li>[http://www.pst.ifi.lmu.de/people/staff/tribastone/ Mirco Tribastone], Ludwig-Maximilians-Universit&#228;t M&#252;nchen <br /> <br><br /> Title: <em>Exact Aggregation for Fluid Process Algebra Models</em><br><br /> Abstract: Recent research in stochastic process algebra has led to efficient fluid approximation techniques obtained by aggregating large populations of sequential components into a single continuous-state variable represented as an ordinary differential equation (ODE). In this talk I will show that, when aggregation is performed higher up in the syntax tree of a model --- i.e., when one is interested in replicas of composite processes --- the resulting ODE system does not scale well with population sizes. I will present two techniques to tackle this problem. The first one is a model-to-model transformation at the process-algebra level. It converts a model with a large ODE system into another one whose size is independent from all population levels, but whose solution is related exactly to that of the original system. Simple syntactic checks are a necessary condition for this transformation to be carried out. The second technique enlarges the class of models amenable to exact aggregation. It performs a transformation directly at the level of the underlying ODE system, which is induced by a novel notion of behavioural equivalence for process algebra with fluid semantics. <br /> </li><br /> </ul></div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=MLQA_2012&diff=408 MLQA 2012 2012-06-25T13:21:23Z

<p>Ender: </p> <hr /> <div><table width="100%" border="0"><br /> <tr><br /> <td><br /> <h1>Joint Workshop on Compositional Modelling and Analysis of Quantitative Systems</h1><br /> <b>September 8, 2012</b><br /> <b>University of Edinburgh</b><br /> </td><br /> <td>&nbsp;</td><br /> <td align="right"><br /> <table width="100%" border="0"><br /> <tr><br /> <td align="right"><br />  </td><br /> </tr></table><br /> [[File:Sicsa.jpg|link=http://www.sicsa.ac.uk/themes/modelling-and-abstraction]]<br /> </td><br /> </tr><br /> </table><br /> <br /> __TOC__<br /> <br /> <hr><br /> <br /> <h3 id="overview">Overview</h3><br /> <br /> <p><br /> The workshop combines the Fourth annual meeting of the [http://wiki.ercim.eu/wg/MLQA ERCIM Working Group on Models and Logics for Quantitative Analysis (MLQA)] with a [http://www.sicsa.ac.uk/themes/modelling-and-abstraction SICSA Modelling and Abstraction Theme] event.<br /> </p><br /> <br /> <p><br /> The theme of the workshop is <em>Compositional Modelling and Analysis of Quantitative Systems</em>. Compositionality is a key concept in both the modeling and analysis of computer systems. It is only by decomposing large complex system into smaller pieces, we can build and analyse these systems.<br /> </p><br /> <br /> <p><br /> The aim of the workshop is to bring together researchers working on quantitative modelling and analysis of computer systems focusing on research using compositional techniques. The workshop hopes to encourage interaction and collaboration between the attendees in developing compositional approaches. <br /> The workshop will bring together MLQA participants from across Europe with contributors to the SICSA theme of 'Modelling and Abstraction'. However, participation from outside MLQA and the SICSA theme are also welcome. <br /> </p><br /> <br /> <p><br /> The workshop will take place immediately following the [http://conferences.ncl.ac.uk/concur-2012/ CONCUR International Conference] taking place in Newcastle-upon-Tyne<br /> 4-7th September 2012.<br /> </p> <br /> <br /> <hr><br /> <br /> <h3 id="speakers">Invited speakers</h3> <br /> <br /> <ul><br /> <li>[http://cs.famaf.unc.edu.ar/~dargenio/ Pedro D'Argenio], FaMAF, Universidad Nacional de Cordoba<br /> <br><br /> <em>Security analysis in probabilistic distributed protocols via bounded reachability</em><br /> </li><br /> <li>[http://www.dsi.unive.it/~marin/ Andrea Marin], Universita di Venezia<br><br /> <em>Compositional model specifications and analyses via product-forms</em></li><br /> <li>[http://wwwhome.cs.utwente.nl/~vdpol/ Jaco van de Pol], University of Twente<br /> <br><br /> <em>Symbolic manipulation of markov automata</em><br /> </li><br /> <li>[http://www.pst.ifi.lmu.de/people/staff/tribastone/ Mirco Tribastone], Ludwig-Maximilians-Universit&#228;t M&#252;nchen <br /> <br><br /> <em>Exact aggregation for fluid process algebra models</em><br /> </li><br /> </ul><br /> <br /> <p><br /> Abstracts of the invited talks are available [[abstractsX|here]].<br /> </p><br /> <br /> <hr><br /> <br /> <h3 id="registration">Registration</h3><br /> <br /> <p><br /> Registration will be at a cost of £25. Registration is free for members of SICSA institutions.<br /> </p><br /> <br /> <hr><br /> <br /> <h3 id="posters">Posters</h3><br /> <br /> <br /> <p><br /> We invited posters under two categories:<br /> </p><br /> <br /> <ul><li><br /> Presentation of recent or on-going work in relation to the themes of MLQA.<br /> </li><br /> <li><br /> Overview of the recent research activities of a research group related to the themes of MLQA.<br /> </li><br /> </ul><br /> <br /> <p><br /> We equally encourage submissions from both research leaders, junior researchers and PhD students.<br /> </p><br /> <br /> <p><br /> Posters should be printed by the <em>participants</em> in their preferred size.<br /> </p><br /> <br /> <p><br /> Notification of your intention to submit, along with a title and short description of the poster, should be sent by <b>August 31</b> to [mailto:gethin.norman@glasgow.ac.uk gethin.norman@glasgow.ac.uk].<br /> </p><br /> <br /> <hr><br /> <br /> <h3 id="programme">Preliminary Programme</h3><br /> <br /> <ul><br /> <li>09:30 - 09:45 <em>Opening</em><br /> </li><br /> <li>09:45 - 10:30 <em>invited talk</em><br /> <br><br><br /> </li><br /> <li>10:30 - 11:00 <em>coffee</em><br /> <br><br><br /> </li><br /> <li>11:00 - 11:45 <em>Invited talk</em><br /> </li><br /> <li>11:45 - 12:30 <em>Invited talk</em><br /> <br><br><br /> </li><br /> <li>12:30 - 14:00 <em>lunch & poster session</em><br /> <br><br><br /> </li><br /> <li>14:00 - 14:30 <em>SICSA Contributed talk</em><br /> </li><br /> <li>14:30 - 15:00 <em>SICSA Contributed talk</em><br /> </li><br /> <li>15:00 - 15:30 <em>SICSA Contributed talk</em><br /> <br><br><br /> </li><br /> <li>15:30 - 16:00 <em>coffee</em><br /> <br><br><br /> </li><br /> <li>16:00 - 17:00 <em>MLQA business meeting</em><br /> </li><br /> </ul><br /> <br /> <hr><br /> <br /> <h3 id="travel">Travel and Accommodation</h3><br /> <br /> <p><br /> The workshop will take place at the<br /> Informatics Forum of the School of Informatics, University of Edinburgh. For details on its location as well as links for travel directions see [http://www.ed.ac.uk/schools-departments/informatics/about/location here]. For those attending CONCUR, Edinburgh is approximately 90 minutes from Newcastle by train.<br /> </p><br /> <br /> <p><br /> For information regarding accommodation will be available soon.<br /> <hr><br /> <br /> <h3 id="organisers">Organisers</h3><br /> <ul><br /> <li>[http://homepages.inf.ed.ac.uk/jeh/ Jane Hilston], University of Edinburgh</li><br /> <li>[http://www.dcs.gla.ac.uk/people/personal/gethin/ Gethin Norman], University of Glasgow</li><br /> </ul><br /> <br /> <hr><br /> <br /> <div id="abstractsX"></div><br /> <h3 id="abstracts">Abstracts of Invited Talks</h3><br /> <br /> <ul><br /> <li>[http://cs.famaf.unc.edu.ar/~dargenio/ Pedro D'Argenio], FaMAF, Universidad Nacional de Cordoba<br /> <br><br /> Title: <em>Security analysis in probabilistic distributed protocols via bounded reachability.<br /> </em><br><br /> Abstract: Probabilistic model checking computes the probability values of a given property quantifying over all possible schedulers (also known as adversaries or policies). It turns out that maximum and minimum probabilities calculated in such a way are overestimations on models of distributed systems in which components are loosely coupled and share little information with each other. The problem exacerbates, if n addition the system is intended to protect private information.<br /> <br><br><br /> In this talk, we will (1) discuss the problem, (2) give a characterization for the set of schedulers that respect the distributed nature of process and the idea of secrecy, (3) report of some important properties of this class of schedulers, and (4) present an algorithm to analyze time-bounded reachability properties based on polynomial optimization. We will briefly discuss a prototype implementation and report some case studies.<br /> <br><br></li><br /> <li>[http://www.dsi.unive.it/~marin/ Andrea Marin], Universita di Venezia<br /> <br><br /> Title: <em>Compositional model specifications and analyses via product-forms</em><br><br /> Abstract: Compositionality is an important aspect of many formalisms used for<br /> quantitative analysis of computer software and hardware architectures<br /> and communication systems. Compositionality allows for the specification <br /> of complex models in terms of cooperations of simpler components in<br /> a modular and hierarchical way. <br /> However, these elegant and often compact model definitions often hide<br /> a huge complexity in the structure of the state space. For models with<br /> underlying continuous or discrete time Markov chains this implies that the quantitative<br /> evaluation of performance and reliability indices cannot rely on<br /> brute force approaches (such as the solution of the set of global balance<br /> equations). Therefore, from the point of view of the<br /> quantitative analysis of compositional models, an approach<br /> that allows one to tackle large state spaces is needed. When<br /> the models are characterised by underlying continuous time Markov<br /> chains (e.g., stochastic Petri nets, Performance Evaluation Process algebra -PEPA-) <br /> product-form theory may be successfully applied. Informally, product-forms<br /> aim at studying the model properties in steady-state starting from the<br /> analysis of its isolated components which are opportunely "parametrised" in order<br /> to take into account the interactions with the remaining parts of the model. <br /> <br><br><br /> After introducing product-form theory in stochastic process algebra<br /> domain, the talk will address the problem of deciding if product-form conditions<br /> are satisfied by the composition of a set of components and how the parameterisation<br /> of these components can be achieved. Special attention will be devoted to the<br /> automation of these steps even in cases of models with infinite state spaces.<br /> The Iterative Numerical Algorithm for Product-forms will be presented. <br /> Concluding remarks will consider the problem of the computation of the <br /> normalising constant and product-form approximations.<br /> <br><br><br /> </li><br /> <br /> <li>[http://www.pst.ifi.lmu.de/people/staff/tribastone/ Mirco Tribastone], Ludwig-Maximilians-Universit&#228;t M&#252;nchen <br /> <br><br /> Title: <em>Exact Aggregation for Fluid Process Algebra Models</em><br><br /> Abstract: Recent research in stochastic process algebra has led to efficient fluid approximation techniques obtained by aggregating large populations of sequential components into a single continuous-state variable represented as an ordinary differential equation (ODE). In this talk I will show that, when aggregation is performed higher up in the syntax tree of a model --- i.e., when one is interested in replicas of composite processes --- the resulting ODE system does not scale well with population sizes. I will present two techniques to tackle this problem. The first one is a model-to-model transformation at the process-algebra level. It converts a model with a large ODE system into another one whose size is independent from all population levels, but whose solution is related exactly to that of the original system. Simple syntactic checks are a necessary condition for this transformation to be carried out. The second technique enlarges the class of models amenable to exact aggregation. It performs a transformation directly at the level of the underlying ODE system, which is induced by a novel notion of behavioural equivalence for process algebra with fluid semantics. <br /> </li><br /> </ul></div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=MLQA_2012&diff=407 MLQA 2012 2012-06-25T13:18:14Z

<p>Ender: </p> <hr /> <div><table width="100%" border="0"><br /> <tr><br /> <td><br /> <h1>Joint Workshop on Compositional Modelling and Analysis of Quantitative Systems</h1><br /> <b>September 8, 2012</b><br /> <b>University of Edinburgh</b><br /> </td><br /> <td>&nbsp;</td><br /> <td align="right"><br /> <table width="100%" border="0"><br /> <tr><br /> <td align="right"><br />  </td><br /> </tr></table><br /> [[File:Sicsa.jpg|link=http://www.sicsa.ac.uk/themes/modelling-and-abstraction]]<br /> </td><br /> </tr><br /> </table><br /> <br /> __TOC__<br /> <br /> <hr><br /> <br /> <h3 id="overview">Overview</h3><br /> <br /> <p><br /> The workshop combines the Fourth annual meeting of the [http://wiki.ercim.eu/wg/MLQA ERCIM Working Group on Models and Logics for Quantitative Analysis (MLQA)] with a [http://www.sicsa.ac.uk/themes/modelling-and-abstraction SICSA Modelling and Abstraction Theme] event.<br /> </p><br /> <br /> <p><br /> The theme of the workshop is <em>Compositional Modelling and Analysis of Quantitative Systems</em>. Compositionality is a key concept in both the modeling and analysis of computer systems. It is only by decomposing large complex system into smaller pieces, we can build and analyse these systems.<br /> </p><br /> <br /> <p><br /> The aim of the workshop is to bring together researchers working on quantitative modelling and analysis of computer systems focusing on research using compositional techniques. The workshop hopes to encourage interaction and collaboration between the attendees in developing compositional approaches. <br /> The workshop will bring together MLQA participants from across Europe with contributors to the SICSA theme of 'Modelling and Abstraction'. However, participation from outside MLQA and the SICSA theme are also welcome. <br /> </p><br /> <br /> <p><br /> The workshop will take place immediately following the [http://conferences.ncl.ac.uk/concur-2012/ CONCUR International Conference] taking place in Newcastle-upon-Tyne<br /> 4-7th September 2012.<br /> </p> <br /> <br /> <hr><br /> <br /> <h3 id="speakers">Invited speakers</h3> <br /> <br /> <ul><br /> <li>[http://cs.famaf.unc.edu.ar/~dargenio/ Pedro D'Argenio], FaMAF, Universidad Nacional de Cordoba<br /> <br><br /> <em>Security analysis in probabilistic distributed protocols via bounded reachability</em><br /> </li><br /> <li>[http://www.dsi.unive.it/~marin/ Andrea Marin], Universita di Venezia<br><br /> <em>Compositional model specifications and analyses via product-forms</em></li><br /> <li>[http://wwwhome.cs.utwente.nl/~vdpol/ Jaco van de Pol], University of Twente<br /> <br><br /> <em>Symbolic manipulation of markov automata</em><br /> </li><br /> <li>[http://www.pst.ifi.lmu.de/people/staff/tribastone/ Mirco Tribastone], Ludwig-Maximilians-Universit&#228;t M&#252;nchen <br /> <br><br /> <em>Exact aggregation for fluid process algebra models</em><br /> </li><br /> </ul><br /> <br /> <p><br /> Abstracts of the invited talks are available [[abstracts|here]].<br /> </p><br /> <br /> <hr><br /> <br /> <h3 id="registration">Registration</h3><br /> <br /> <p><br /> Registration will be at a cost of £25. Registration is free for members of SICSA institutions.<br /> </p><br /> <br /> <hr><br /> <br /> <h3 id="posters">Posters</h3><br /> <br /> <br /> <p><br /> We invited posters under two categories:<br /> </p><br /> <br /> <ul><li><br /> Presentation of recent or on-going work in relation to the themes of MLQA.<br /> </li><br /> <li><br /> Overview of the recent research activities of a research group related to the themes of MLQA.<br /> </li><br /> </ul><br /> <br /> <p><br /> We equally encourage submissions from both research leaders, junior researchers and PhD students.<br /> </p><br /> <br /> <p><br /> Posters should be printed by the <em>participants</em> in their preferred size.<br /> </p><br /> <br /> <p><br /> Notification of your intention to submit, along with a title and short description of the poster, should be sent by <b>August 31</b> to [mailto:gethin.norman@glasgow.ac.uk gethin.norman@glasgow.ac.uk].<br /> </p><br /> <br /> <hr><br /> <br /> <h3 id="programme">Preliminary Programme</h3><br /> <br /> <ul><br /> <li>09:30 - 09:45 <em>Opening</em><br /> </li><br /> <li>09:45 - 10:30 <em>invited talk</em><br /> <br><br><br /> </li><br /> <li>10:30 - 11:00 <em>coffee</em><br /> <br><br><br /> </li><br /> <li>11:00 - 11:45 <em>Invited talk</em><br /> </li><br /> <li>11:45 - 12:30 <em>Invited talk</em><br /> <br><br><br /> </li><br /> <li>12:30 - 14:00 <em>lunch & poster session</em><br /> <br><br><br /> </li><br /> <li>14:00 - 14:30 <em>SICSA Contributed talk</em><br /> </li><br /> <li>14:30 - 15:00 <em>SICSA Contributed talk</em><br /> </li><br /> <li>15:00 - 15:30 <em>SICSA Contributed talk</em><br /> <br><br><br /> </li><br /> <li>15:30 - 16:00 <em>coffee</em><br /> <br><br><br /> </li><br /> <li>16:00 - 17:00 <em>MLQA business meeting</em><br /> </li><br /> </ul><br /> <br /> <hr><br /> <br /> <h3 id="travel">Travel and Accommodation</h3><br /> <br /> <p><br /> The workshop will take place at the<br /> Informatics Forum of the School of Informatics, University of Edinburgh. For details on its location as well as links for travel directions see [http://www.ed.ac.uk/schools-departments/informatics/about/location here]. For those attending CONCUR, Edinburgh is approximately 90 minutes from Newcastle by train.<br /> </p><br /> <br /> <p><br /> For information regarding accommodation will be available soon.<br /> <hr><br /> <br /> <h3 id="organisers">Organisers</h3><br /> <ul><br /> <li>[http://homepages.inf.ed.ac.uk/jeh/ Jane Hilston], University of Edinburgh</li><br /> <li>[http://www.dcs.gla.ac.uk/people/personal/gethin/ Gethin Norman], University of Glasgow</li><br /> </ul><br /> <br /> <hr><br /> <br /> <div id="abstracts"></div><br /> <h3 id="abstracts">Abstracts of Invited Talks</h3><br /> <br /> <ul><br /> <li>[http://cs.famaf.unc.edu.ar/~dargenio/ Pedro D'Argenio], FaMAF, Universidad Nacional de Cordoba<br /> <br><br /> Title: <em>Security analysis in probabilistic distributed protocols via bounded reachability.<br /> </em><br><br /> Abstract: Probabilistic model checking computes the probability values of a given property quantifying over all possible schedulers (also known as adversaries or policies). It turns out that maximum and minimum probabilities calculated in such a way are overestimations on models of distributed systems in which components are loosely coupled and share little information with each other. The problem exacerbates, if n addition the system is intended to protect private information.<br /> <br><br><br /> In this talk, we will (1) discuss the problem, (2) give a characterization for the set of schedulers that respect the distributed nature of process and the idea of secrecy, (3) report of some important properties of this class of schedulers, and (4) present an algorithm to analyze time-bounded reachability properties based on polynomial optimization. We will briefly discuss a prototype implementation and report some case studies.<br /> <br><br></li><br /> <li>[http://www.dsi.unive.it/~marin/ Andrea Marin], Universita di Venezia<br /> <br><br /> Title: <em>Compositional model specifications and analyses via product-forms</em><br><br /> Abstract: Compositionality is an important aspect of many formalisms used for<br /> quantitative analysis of computer software and hardware architectures<br /> and communication systems. Compositionality allows for the specification <br /> of complex models in terms of cooperations of simpler components in<br /> a modular and hierarchical way. <br /> However, these elegant and often compact model definitions often hide<br /> a huge complexity in the structure of the state space. For models with<br /> underlying continuous or discrete time Markov chains this implies that the quantitative<br /> evaluation of performance and reliability indices cannot rely on<br /> brute force approaches (such as the solution of the set of global balance<br /> equations). Therefore, from the point of view of the<br /> quantitative analysis of compositional models, an approach<br /> that allows one to tackle large state spaces is needed. When<br /> the models are characterised by underlying continuous time Markov<br /> chains (e.g., stochastic Petri nets, Performance Evaluation Process algebra -PEPA-) <br /> product-form theory may be successfully applied. Informally, product-forms<br /> aim at studying the model properties in steady-state starting from the<br /> analysis of its isolated components which are opportunely "parametrised" in order<br /> to take into account the interactions with the remaining parts of the model. <br /> <br><br><br /> After introducing product-form theory in stochastic process algebra<br /> domain, the talk will address the problem of deciding if product-form conditions<br /> are satisfied by the composition of a set of components and how the parameterisation<br /> of these components can be achieved. Special attention will be devoted to the<br /> automation of these steps even in cases of models with infinite state spaces.<br /> The Iterative Numerical Algorithm for Product-forms will be presented. <br /> Concluding remarks will consider the problem of the computation of the <br /> normalising constant and product-form approximations.<br /> <br><br><br /> </li><br /> <br /> <li>[http://www.pst.ifi.lmu.de/people/staff/tribastone/ Mirco Tribastone], Ludwig-Maximilians-Universit&#228;t M&#252;nchen <br /> <br><br /> Title: <em>Exact Aggregation for Fluid Process Algebra Models</em><br><br /> Abstract: Recent research in stochastic process algebra has led to efficient fluid approximation techniques obtained by aggregating large populations of sequential components into a single continuous-state variable represented as an ordinary differential equation (ODE). In this talk I will show that, when aggregation is performed higher up in the syntax tree of a model --- i.e., when one is interested in replicas of composite processes --- the resulting ODE system does not scale well with population sizes. I will present two techniques to tackle this problem. The first one is a model-to-model transformation at the process-algebra level. It converts a model with a large ODE system into another one whose size is independent from all population levels, but whose solution is related exactly to that of the original system. Simple syntactic checks are a necessary condition for this transformation to be carried out. The second technique enlarges the class of models amenable to exact aggregation. It performs a transformation directly at the level of the underlying ODE system, which is induced by a novel notion of behavioural equivalence for process algebra with fluid semantics. <br /> </li><br /> </ul></div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=Main_Page&diff=406 Main Page 2012-06-24T16:58:24Z

<p>Ender: /* Upcoming events */</p> <hr /> <div>== ERCIM Working Group on Models and Logics for Quantitative Analysis (MLQA) ==<br /> <br /> [[Image:Image002.png|frame]] Models and Logics for Quantitative Analysis are seen as comprising process models analysed using logics for quantitative properties. More specifically, we will<br /> <br /> # consider process models formally described by transition systems, automata or process calculi,<br /> # consider logics for expressing stochastic and continuous properties as well as discrete ones,<br /> # focus on algorithms, theory and tools, and<br /> # study applications with particular emphasis on embedded systems and service oriented systems but will aim at treating also IT guided workflow systems and biological systems.<br /> <br /> The MLQA home page: http://wiki.ercim.eu/wg/MLQA<br /> <br /> The goal of this working group is to create a venue for knowledge sharing in this exciting area, for creating a network also for young researchers, for sharing tools developed within the field, for discussing research directions, and eventually to formulate a European project or network on formal quantitative analysis.<br /> <br /> The working group will be open also to researchers outside of ERCIM (and outside of Europe).<br /> <br /> == Upcoming events ==<br /> <br /> <span style="color: red;">The fourth annual meeting: [[MLQA 2012]], Edinburgh, UK.</span><br /> <br /> The fifth annual meeting: [[MLQA 2013]], Rome, Italy.<br /> <br /> == Past events ==<br /> <br /> The Kick-Off meeting: [[MLQA 2009|MLQA 2009]], York, UK.<br /> <br /> The second annual meeting: [[MLQA 2010|MLQA 2010]], Edinburgh, UK.<br /> <br /> The third annual meeting: [[MLQA 2011|MLQA 2011]], Aachen, Germany.</div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=Main_Page&diff=405 Main Page 2012-06-24T16:57:30Z

<p>Ender: /* Upcoming events */</p> <hr /> <div>== ERCIM Working Group on Models and Logics for Quantitative Analysis (MLQA) ==<br /> <br /> [[Image:Image002.png|frame]] Models and Logics for Quantitative Analysis are seen as comprising process models analysed using logics for quantitative properties. More specifically, we will<br /> <br /> # consider process models formally described by transition systems, automata or process calculi,<br /> # consider logics for expressing stochastic and continuous properties as well as discrete ones,<br /> # focus on algorithms, theory and tools, and<br /> # study applications with particular emphasis on embedded systems and service oriented systems but will aim at treating also IT guided workflow systems and biological systems.<br /> <br /> The MLQA home page: http://wiki.ercim.eu/wg/MLQA<br /> <br /> The goal of this working group is to create a venue for knowledge sharing in this exciting area, for creating a network also for young researchers, for sharing tools developed within the field, for discussing research directions, and eventually to formulate a European project or network on formal quantitative analysis.<br /> <br /> The working group will be open also to researchers outside of ERCIM (and outside of Europe).<br /> <br /> == Upcoming events ==<br /> <br /> <pre style="color:red">The fourth annual meeting: [[MLQA 2012]], Edinburgh, UK.</pre><br /> <br /> The fifth annual meeting: [[MLQA 2013]], Rome, Italy.<br /> <br /> == Past events ==<br /> <br /> The Kick-Off meeting: [[MLQA 2009|MLQA 2009]], York, UK.<br /> <br /> The second annual meeting: [[MLQA 2010|MLQA 2010]], Edinburgh, UK.<br /> <br /> The third annual meeting: [[MLQA 2011|MLQA 2011]], Aachen, Germany.</div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=MLQA_2012&diff=404 MLQA 2012 2012-06-24T16:56:02Z

<p>Ender: </p> <hr /> <div><table width="100%" border="0"><br /> <tr><br /> <td><br /> <h1>Joint Workshop on Compositional Modelling and Analysis of Quantitative Systems</h1><br /> <b>September 8, 2012</b><br /> <b>University of Edinburgh</b><br /> </td><br /> <td>&nbsp;</td><br /> <td align="right"><br /> <table width="100%" border="0"><br /> <tr><br /> <td align="right"><br />  </td><br /> </tr></table><br /> [[File:Sicsa.jpg|link=http://www.sicsa.ac.uk/themes/modelling-and-abstraction]]<br /> </td><br /> </tr><br /> </table><br /> <br /> __TOC__<br /> <br /> <hr><br /> <br /> <h3 id="overview">Overview</h3><br /> <br /> <p><br /> The workshop combines the Fourth annual meeting of the [http://wiki.ercim.eu/wg/MLQA ERCIM Working Group on Models and Logics for Quantitative Analysis (MLQA)] with a [http://www.sicsa.ac.uk/themes/modelling-and-abstraction SICSA Modelling and Abstraction Theme] event.<br /> </p><br /> <br /> <p><br /> The theme of the workshop is <em>Compositional Modelling and Analysis of Quantitative Systems</em>. Compositionality is a key concept in both the modeling and analysis of computer systems. It is only by decomposing large complex system into smaller pieces, we can build and analyse these systems.<br /> </p><br /> <br /> <p><br /> The aim of the workshop is to bring together researchers working on quantitative modelling and analysis of computer systems focusing on research using compositional techniques. The workshop hopes to encourage interaction and collaboration between the attendees in developing compositional approaches. <br /> The workshop will bring together MLQA participants from across Europe with contributors to the SICSA theme of 'Modelling and Abstraction'. However, participation from outside MLQA and the SICSA theme are also welcome. <br /> </p><br /> <br /> <p><br /> The workshop will take place immediately following the [http://conferences.ncl.ac.uk/concur-2012/ CONCUR International Conference] taking place in Newcastle-upon-Tyne<br /> 4-7th September 2012.<br /> </p> <br /> <br /> <hr><br /> <br /> <h3 id="speakers">Invited speakers</h3> <br /> <br /> <ul><br /> <li>[http://cs.famaf.unc.edu.ar/~dargenio/ Pedro D'Argenio], FaMAF, Universidad Nacional de Cordoba<br /> <br><br /> <em>Security analysis in probabilistic distributed protocols via bounded reachability</em><br /> </li><br /> <li>[http://www.dsi.unive.it/~marin/ Andrea Marin], Universita di Venezia<br><br /> <em>Compositional model specifications and analyses via product-forms</em></li><br /> <li>[http://wwwhome.cs.utwente.nl/~vdpol/ Jaco van de Pol], University of Twente<br /> <br><br /> <em>tbc</em><br /> </li><br /> <li>[http://www.pst.ifi.lmu.de/people/staff/tribastone/ Mirco Tribastone], Ludwig-Maximilians-Universit&#228;t M&#252;nchen <br /> <br><br /> <em>Exact Aggregation for Fluid Process Algebra Models</em><br /> </li><br /> </ul><br /> <br /> <p><br /> Abstracts of the invited talks are available [[abstracts|here]].<br /> </p><br /> <br /> <hr><br /> <br /> <h3 id="registration">Registration</h3><br /> <br /> <p><br /> Registration will be at a cost of £25. Registration is free for members of SICSA institutions.<br /> </p><br /> <br /> <hr><br /> <br /> <h3 id="posters">Posters</h3><br /> <br /> <br /> <p><br /> We invited posters under two categories:<br /> </p><br /> <br /> <ul><li><br /> Presentation of recent or on-going work in relation to the themes of MLQA.<br /> </li><br /> <li><br /> Overview of the recent research activities of a research group related to the themes of MLQA.<br /> </li><br /> </ul><br /> <br /> <p><br /> We equally encourage submissions from both research leaders, junior researchers and PhD students.<br /> </p><br /> <br /> <p><br /> Posters should be printed by the <em>participants</em> in their preferred size.<br /> </p><br /> <br /> <p><br /> Notification of your intention to submit, along with a title and short description of the poster, should be sent by <b>August 31</b> to [mailto:gethin.norman@glasgow.ac.uk gethin.norman@glasgow.ac.uk].<br /> </p><br /> <br /> <hr><br /> <br /> <h3 id="programme">Preliminary Programme</h3><br /> <br /> <ul><br /> <li>09:30 - 09:45 <em>Opening</em><br /> </li><br /> <li>09:45 - 10:30 <em>invited talk</em><br /> <br><br><br /> </li><br /> <li>10:30 - 11:00 <em>coffee</em><br /> <br><br><br /> </li><br /> <li>11:00 - 11:45 <em>Invited talk</em><br /> </li><br /> <li>11:45 - 12:30 <em>Invited talk</em><br /> <br><br><br /> </li><br /> <li>12:30 - 14:00 <em>lunch & poster session</em><br /> <br><br><br /> </li><br /> <li>14:00 - 14:30 <em>SICSA Contributed talk</em><br /> </li><br /> <li>14:30 - 15:00 <em>SICSA Contributed talk</em><br /> </li><br /> <li>15:00 - 15:30 <em>SICSA Contributed talk</em><br /> <br><br><br /> </li><br /> <li>15:30 - 16:00 <em>coffee</em><br /> <br><br><br /> </li><br /> <li>16:00 - 17:00 <em>MLQA business meeting</em><br /> </li><br /> </ul><br /> <br /> <hr><br /> <br /> <h3 id="travel">Travel and Accommodation</h3><br /> <br /> <p><br /> The workshop will take place at the<br /> Informatics Forum of the School of Informatics, University of Edinburgh. For details on its location as well as links for travel directions see [http://www.ed.ac.uk/schools-departments/informatics/about/location here]. For those attending CONCUR, Edinburgh is approximately 90 minutes from Newcastle by train.<br /> </p><br /> <br /> <p><br /> For information regarding accommodation will be available soon.<br /> <hr><br /> <br /> <h3 id="organisers">Organisers</h3><br /> <ul><br /> <li>[http://homepages.inf.ed.ac.uk/jeh/ Jane Hilston], University of Edinburgh</li><br /> <li>[http://www.dcs.gla.ac.uk/people/personal/gethin/ Gethin Norman], University of Glasgow</li><br /> </ul><br /> <br /> <hr><br /> <br /> <div id="abstracts"></div><br /> <h3 id="abstracts">Abstracts of Invited Talks</h3><br /> <br /> <ul><br /> <li>[http://cs.famaf.unc.edu.ar/~dargenio/ Pedro D'Argenio], FaMAF, Universidad Nacional de Cordoba<br /> <br><br /> Title: <em>Security analysis in probabilistic distributed protocols via bounded reachability.<br /> </em><br><br /> Abstract: Probabilistic model checking computes the probability values of a given property quantifying over all possible schedulers (also known as adversaries or policies). It turns out that maximum and minimum probabilities calculated in such a way are overestimations on models of distributed systems in which components are loosely coupled and share little information with each other. The problem exacerbates, if n addition the system is intended to protect private information.<br /> <br><br><br /> In this talk, we will (1) discuss the problem, (2) give a characterization for the set of schedulers that respect the distributed nature of process and the idea of secrecy, (3) report of some important properties of this class of schedulers, and (4) present an algorithm to analyze time-bounded reachability properties based on polynomial optimization. We will briefly discuss a prototype implementation and report some case studies.<br /> <br><br></li><br /> <li>[http://www.dsi.unive.it/~marin/ Andrea Marin], Universita di Venezia<br /> <br><br /> Title: <em>Compositional model specifications and analyses via product-forms</em><br><br /> Abstract: Compositionality is an important aspect of many formalisms used for<br /> quantitative analysis of computer software and hardware architectures<br /> and communication systems. Compositionality allows for the specification <br /> of complex models in terms of cooperations of simpler components in<br /> a modular and hierarchical way. <br /> However, these elegant and often compact model definitions often hide<br /> a huge complexity in the structure of the state space. For models with<br /> underlying continuous or discrete time Markov chains this implies that the quantitative<br /> evaluation of performance and reliability indices cannot rely on<br /> brute force approaches (such as the solution of the set of global balance<br /> equations). Therefore, from the point of view of the<br /> quantitative analysis of compositional models, an approach<br /> that allows one to tackle large state spaces is needed. When<br /> the models are characterised by underlying continuous time Markov<br /> chains (e.g., stochastic Petri nets, Performance Evaluation Process algebra -PEPA-) <br /> product-form theory may be successfully applied. Informally, product-forms<br /> aim at studying the model properties in steady-state starting from the<br /> analysis of its isolated components which are opportunely "parametrised" in order<br /> to take into account the interactions with the remaining parts of the model. <br /> <br><br><br /> After introducing product-form theory in stochastic process algebra<br /> domain, the talk will address the problem of deciding if product-form conditions<br /> are satisfied by the composition of a set of components and how the parameterisation<br /> of these components can be achieved. Special attention will be devoted to the<br /> automation of these steps even in cases of models with infinite state spaces.<br /> The Iterative Numerical Algorithm for Product-forms will be presented. <br /> Concluding remarks will consider the problem of the computation of the <br /> normalising constant and product-form approximations.<br /> <br><br><br /> </li><br /> <br /> <li>[http://www.pst.ifi.lmu.de/people/staff/tribastone/ Mirco Tribastone], Ludwig-Maximilians-Universit&#228;t M&#252;nchen <br /> <br><br /> Title: <em>Exact Aggregation for Fluid Process Algebra Models</em><br><br /> Abstract: Recent research in stochastic process algebra has led to efficient fluid approximation techniques obtained by aggregating large populations of sequential components into a single continuous-state variable represented as an ordinary differential equation (ODE). In this talk I will show that, when aggregation is performed higher up in the syntax tree of a model --- i.e., when one is interested in replicas of composite processes --- the resulting ODE system does not scale well with population sizes. I will present two techniques to tackle this problem. The first one is a model-to-model transformation at the process-algebra level. It converts a model with a large ODE system into another one whose size is independent from all population levels, but whose solution is related exactly to that of the original system. Simple syntactic checks are a necessary condition for this transformation to be carried out. The second technique enlarges the class of models amenable to exact aggregation. It performs a transformation directly at the level of the underlying ODE system, which is induced by a novel notion of behavioural equivalence for process algebra with fluid semantics. <br /> </li><br /> </ul></div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=MLQA_2012&diff=403 MLQA 2012 2012-06-24T16:35:38Z

<p>Ender: </p> <hr /> <div><table width="100%" border="0"><br /> <tr><br /> <td><br /> <h1>Joint Workshop on Compositional Modelling and Analysis of Quantitative Systems</h1><br /> <b>September 8, 2012</b><br /> <b>University of Edinburgh</b><br /> </td><br /> <td>&nbsp;</td><br /> <td align="right"><br /> <table width="100%" border="0"><br /> <tr><br /> <td align="right"><br />  </td><br /> </tr></table><br /> [[File:Sicsa.jpg|link=http://www.sicsa.ac.uk/themes/modelling-and-abstraction]]<br /> </td><br /> </tr><br /> </table><br /> <br /> <br /> <br /> <hr><br /> <br /> <h3 id="overview">Overview</h3><br /> <br /> <p><br /> The workshop combines the Fourth annual meeting of the [http://wiki.ercim.eu/wg/MLQA ERCIM Working Group on Models and Logics for Quantitative Analysis (MLQA)] with a [http://www.sicsa.ac.uk/themes/modelling-and-abstraction SICSA Modelling and Abstraction Theme] event.<br /> </p><br /> <br /> <p><br /> The theme of the workshop is <em>Compositional Modelling and Analysis of Quantitative Systems</em>. Compositionality is a key concept in both the modeling and analysis of computer systems. It is only by decomposing large complex system into smaller pieces, we can build and analyse these systems.<br /> </p><br /> <br /> <p><br /> The aim of the workshop is to bring together researchers working on quantitative modelling and analysis of computer systems focusing on research using compositional techniques. The workshop hopes to encourage interaction and collaboration between the attendees in developing compositional approaches. <br /> The workshop will bring together MLQA participants from across Europe with contributors to the SICSA theme of 'Modelling and Abstraction'. However, participation from outside MLQA and the SICSA theme are also welcome. <br /> </p><br /> <br /> <p><br /> The workshop will take place immediately following the [http://conferences.ncl.ac.uk/concur-2012/ CONCUR International Conference] taking place in Newcastle-upon-Tyne<br /> 4-7th September 2012.<br /> </p> <br /> <br /> <hr><br /> <br /> <h3 id="speakers">Invited speakers</h3> <br /> <br /> <ul><br /> <li>[http://cs.famaf.unc.edu.ar/~dargenio/ Pedro D'Argenio], FaMAF, Universidad Nacional de Cordoba<br /> <br><br /> <em>Security analysis in probabilistic distributed protocols via bounded reachability</em><br /> </li><br /> <li>[http://www.dsi.unive.it/~marin/ Andrea Marin], Universita di Venezia<br><br /> <em>Compositional model specifications and analyses via product-forms</em></li><br /> <li>[http://wwwhome.cs.utwente.nl/~vdpol/ Jaco van de Pol], University of Twente<br /> <br><br /> <em>tbc</em><br /> </li><br /> <li>[http://www.pst.ifi.lmu.de/people/staff/tribastone/ Mirco Tribastone], Ludwig-Maximilians-Universit&#228;t M&#252;nchen <br /> <br><br /> <em>Exact Aggregation for Fluid Process Algebra Models</em><br /> </li><br /> </ul><br /> <br /> <p><br /> Abstracts of the invited talks are available [[abstracts|here]].<br /> </p><br /> <br /> <hr><br /> <br /> <h3 id="registration">Registration</h3><br /> <br /> <p><br /> Registration will be at a cost of £25. Registration is free for members of SICSA institutions.<br /> </p><br /> <br /> <hr><br /> <br /> <h3 id="posters">Posters</h3><br /> <br /> <br /> <p><br /> We invited posters under two categories:<br /> </p><br /> <br /> <ul><li><br /> Presentation of recent or on-going work in relation to the themes of MLQA.<br /> </li><br /> <li><br /> Overview of the recent research activities of a research group related to the themes of MLQA.<br /> </li><br /> </ul><br /> <br /> <p><br /> We equally encourage submissions from both research leaders, junior researchers and PhD students.<br /> </p><br /> <br /> <p><br /> Posters should be printed by the <em>participants</em> in their preferred size.<br /> </p><br /> <br /> <p><br /> Notification of your intention to submit, along with a title and short description of the poster, should be sent by <b>August 31</b> to [mailto:gethin.norman@glasgow.ac.uk gethin.norman@glasgow.ac.uk].<br /> </p><br /> <br /> <hr><br /> <br /> <h3 id="programme">Preliminary Programme</h3><br /> <br /> <ul><br /> <li>09:30 - 09:45 <em>Opening</em><br /> </li><br /> <li>09:45 - 10:30 <em>invited talk</em><br /> <br><br><br /> </li><br /> <li>10:30 - 11:00 <em>coffee</em><br /> <br><br><br /> </li><br /> <li>11:00 - 11:45 <em>Invited talk</em><br /> </li><br /> <li>11:45 - 12:30 <em>Invited talk</em><br /> <br><br><br /> </li><br /> <li>12:30 - 14:00 <em>lunch & poster session</em><br /> <br><br><br /> </li><br /> <li>14:00 - 14:30 <em>SICSA Contributed talk</em><br /> </li><br /> <li>14:30 - 15:00 <em>SICSA Contributed talk</em><br /> </li><br /> <li>15:00 - 15:30 <em>SICSA Contributed talk</em><br /> <br><br><br /> </li><br /> <li>15:30 - 16:00 <em>coffee</em><br /> <br><br><br /> </li><br /> <li>16:00 - 17:00 <em>MLQA business meeting</em><br /> </li><br /> </ul><br /> <br /> <hr><br /> <br /> <h3 id="travel">Travel and Accommodation</h3><br /> <br /> <p><br /> The workshop will take place at the<br /> Informatics Forum of the School of Informatics, University of Edinburgh. For details on its location as well as links for travel directions see [http://www.ed.ac.uk/schools-departments/informatics/about/location here]. For those attending CONCUR, Edinburgh is approximately 90 minutes from Newcastle by train.<br /> </p><br /> <br /> <p><br /> For information regarding accommodation will be available soon.<br /> <hr><br /> <br /> <h3 id="organisers">Organisers</h3><br /> <ul><br /> <li>[http://homepages.inf.ed.ac.uk/jeh/ Jane Hilston], University of Edinburgh</li><br /> <li>[http://www.dcs.gla.ac.uk/people/personal/gethin/ Gethin Norman], University of Glasgow</li><br /> </ul><br /> <br /> <hr><br /> <br /> <div id="abstracts"></div><br /> <h3 id="abstracts">Abstracts of Invited Talks</h3><br /> <br /> <ul><br /> <li>[http://cs.famaf.unc.edu.ar/~dargenio/ Pedro D'Argenio], FaMAF, Universidad Nacional de Cordoba<br /> <br><br /> Title: <em>Security analysis in probabilistic distributed protocols via bounded reachability.<br /> </em><br><br /> Abstract: Probabilistic model checking computes the probability values of a given property quantifying over all possible schedulers (also known as adversaries or policies). It turns out that maximum and minimum probabilities calculated in such a way are overestimations on models of distributed systems in which components are loosely coupled and share little information with each other. The problem exacerbates, if n addition the system is intended to protect private information.<br /> <br><br><br /> In this talk, we will (1) discuss the problem, (2) give a characterization for the set of schedulers that respect the distributed nature of process and the idea of secrecy, (3) report of some important properties of this class of schedulers, and (4) present an algorithm to analyze time-bounded reachability properties based on polynomial optimization. We will briefly discuss a prototype implementation and report some case studies.<br /> <br><br></li><br /> <li>[http://www.dsi.unive.it/~marin/ Andrea Marin], Universita di Venezia<br /> <br><br /> Title: <em>Compositional model specifications and analyses via product-forms</em><br><br /> Abstract: Compositionality is an important aspect of many formalisms used for<br /> quantitative analysis of computer software and hardware architectures<br /> and communication systems. Compositionality allows for the specification <br /> of complex models in terms of cooperations of simpler components in<br /> a modular and hierarchical way. <br /> However, these elegant and often compact model definitions often hide<br /> a huge complexity in the structure of the state space. For models with<br /> underlying continuous or discrete time Markov chains this implies that the quantitative<br /> evaluation of performance and reliability indices cannot rely on<br /> brute force approaches (such as the solution of the set of global balance<br /> equations). Therefore, from the point of view of the<br /> quantitative analysis of compositional models, an approach<br /> that allows one to tackle large state spaces is needed. When<br /> the models are characterised by underlying continuous time Markov<br /> chains (e.g., stochastic Petri nets, Performance Evaluation Process algebra -PEPA-) <br /> product-form theory may be successfully applied. Informally, product-forms<br /> aim at studying the model properties in steady-state starting from the<br /> analysis of its isolated components which are opportunely "parametrised" in order<br /> to take into account the interactions with the remaining parts of the model. <br /> <br><br><br /> After introducing product-form theory in stochastic process algebra<br /> domain, the talk will address the problem of deciding if product-form conditions<br /> are satisfied by the composition of a set of components and how the parameterisation<br /> of these components can be achieved. Special attention will be devoted to the<br /> automation of these steps even in cases of models with infinite state spaces.<br /> The Iterative Numerical Algorithm for Product-forms will be presented. <br /> Concluding remarks will consider the problem of the computation of the <br /> normalising constant and product-form approximations.<br /> <br><br><br /> </li><br /> <br /> <li>[http://www.pst.ifi.lmu.de/people/staff/tribastone/ Mirco Tribastone], Ludwig-Maximilians-Universit&#228;t M&#252;nchen <br /> <br><br /> Title: <em>Exact Aggregation for Fluid Process Algebra Models</em><br><br /> Abstract: Recent research in stochastic process algebra has led to efficient fluid approximation techniques obtained by aggregating large populations of sequential components into a single continuous-state variable represented as an ordinary differential equation (ODE). In this talk I will show that, when aggregation is performed higher up in the syntax tree of a model --- i.e., when one is interested in replicas of composite processes --- the resulting ODE system does not scale well with population sizes. I will present two techniques to tackle this problem. The first one is a model-to-model transformation at the process-algebra level. It converts a model with a large ODE system into another one whose size is independent from all population levels, but whose solution is related exactly to that of the original system. Simple syntactic checks are a necessary condition for this transformation to be carried out. The second technique enlarges the class of models amenable to exact aggregation. It performs a transformation directly at the level of the underlying ODE system, which is induced by a novel notion of behavioural equivalence for process algebra with fluid semantics. <br /> </li><br /> </ul></div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=MLQA_2012&diff=402 MLQA 2012 2012-06-24T16:24:02Z

<p>Ender: </p> <hr /> <div><table width="100%" border="0"><br /> <tr><br /> <td><br /> <h1>Joint Workshop on Compositional Modelling and Analysis of Quantitative Systems</h1><br /> <h2>September 8, 2012</h2><br /> <h2>University of Edinburgh</h2><br /> </td><br /> <td>&nbsp;</td><br /> <td align="right"><br /> <table width="100%" border="0"><br /> <tr><br /> <td align="right"><br />  </td><br /> </tr></table><br /> [[File:Sicsa.jpg|link=http://www.sicsa.ac.uk/themes/modelling-and-abstraction]]<br /> </td><br /> </tr><br /> </table><br /> <br /> <hr><br /> <br /> <br /> <br /> <br /> <br /> <hr><br /> <br /> <h3 id="overview">Overview</h3><br /> <br /> <p><br /> The workshop combines the Fourth annual meeting of the [http://wiki.ercim.eu/wg/MLQA ERCIM Working Group on Models and Logics for Quantitative Analysis (MLQA)] with a [http://www.sicsa.ac.uk/themes/modelling-and-abstraction SICSA Modelling and Abstraction Theme] event.<br /> </p><br /> <br /> <p><br /> The theme of the workshop is <em>Compositional Modelling and Analysis of Quantitative Systems</em>. Compositionality is a key concept in both the modeling and analysis of computer systems. It is only by decomposing large complex system into smaller pieces, we can build and analyse these systems.<br /> </p><br /> <br /> <p><br /> The aim of the workshop is to bring together researchers working on quantitative modelling and analysis of computer systems focusing on research using compositional techniques. The workshop hopes to encourage interaction and collaboration between the attendees in developing compositional approaches. <br /> The workshop will bring together MLQA participants from across Europe with contributors to the SICSA theme of 'Modelling and Abstraction'. However, participation from outside MLQA and the SICSA theme are also welcome. <br /> </p><br /> <br /> <p><br /> The workshop will take place immediately following the [http://conferences.ncl.ac.uk/concur-2012/ CONCUR International Conference] taking place in Newcastle-upon-Tyne<br /> 4-7th September 2012.<br /> </p> <br /> <br /> <hr><br /> <br /> <h3 id="speakers">Invited speakers</h3> <br /> <br /> <ul><br /> <li>[http://cs.famaf.unc.edu.ar/~dargenio/ Pedro D'Argenio], FaMAF, Universidad Nacional de Cordoba<br /> <br><br /> <em>Security analysis in probabilistic distributed protocols via bounded reachability</em><br /> </li><br /> <li>[http://www.dsi.unive.it/~marin/ Andrea Marin], Universita di Venezia<br><br /> <em>Compositional model specifications and analyses via product-forms</em></li><br /> <li>[http://wwwhome.cs.utwente.nl/~vdpol/ Jaco van de Pol], University of Twente<br /> <br><br /> <em>tbc</em><br /> </li><br /> <li>[http://www.pst.ifi.lmu.de/people/staff/tribastone/ Mirco Tribastone], Ludwig-Maximilians-Universit&#228;t M&#252;nchen <br /> <br><br /> <em>Exact Aggregation for Fluid Process Algebra Models</em><br /> </li><br /> </ul><br /> <br /> <p><br /> Abstracts of the invited talks are available [[abstracts|here]].<br /> </p><br /> <br /> <hr><br /> <br /> <h3 id="registration">Registration</h3><br /> <br /> <p><br /> Registration will be at a cost of £25. Registration is free for members of SICSA institutions.<br /> </p><br /> <br /> <hr><br /> <br /> <h3 id="posters">Posters</h3><br /> <br /> <br /> <p><br /> We invited posters under two categories:<br /> </p><br /> <br /> <ul><li><br /> Presentation of recent or on-going work in relation to the themes of MLQA.<br /> </li><br /> <li><br /> Overview of the recent research activities of a research group related to the themes of MLQA.<br /> </li><br /> </ul><br /> <br /> <p><br /> We equally encourage submissions from both research leaders, junior researchers and PhD students.<br /> </p><br /> <br /> <p><br /> Posters should be printed by the <em>participants</em> in their preferred size.<br /> </p><br /> <br /> <p><br /> Notification of your intention to submit, along with a title and short description of the poster, should be sent by <b>August 31</b> to [mailto:gethin.norman@glasgow.ac.uk gethin.norman@glasgow.ac.uk].<br /> </p><br /> <br /> <hr><br /> <br /> <h3 id="programme">Preliminary Programme</h3><br /> <br /> <ul><br /> <li>09:30 - 09:45 <em>Opening</em><br /> </li><br /> <li>09:45 - 10:30 <em>invited talk</em><br /> <br><br><br /> </li><br /> <li>10:30 - 11:00 <em>coffee</em><br /> <br><br><br /> </li><br /> <li>11:00 - 11:45 <em>Invited talk</em><br /> </li><br /> <li>11:45 - 12:30 <em>Invited talk</em><br /> <br><br><br /> </li><br /> <li>12:30 - 14:00 <em>lunch & poster session</em><br /> <br><br><br /> </li><br /> <li>14:00 - 14:30 <em>SICSA Contributed talk</em><br /> </li><br /> <li>14:30 - 15:00 <em>SICSA Contributed talk</em><br /> </li><br /> <li>15:00 - 15:30 <em>SICSA Contributed talk</em><br /> <br><br><br /> </li><br /> <li>15:30 - 16:00 <em>coffee</em><br /> <br><br><br /> </li><br /> <li>16:00 - 17:00 <em>MLQA business meeting</em><br /> </li><br /> </ul><br /> <br /> <hr><br /> <br /> <h3 id="travel">Travel and Accommodation</h3><br /> <br /> <p><br /> The workshop will take place at the<br /> Informatics Forum of the School of Informatics, University of Edinburgh. For details on its location as well as links for travel directions see [http://www.ed.ac.uk/schools-departments/informatics/about/location here]. For those attending CONCUR, Edinburgh is approximately 90 minutes from Newcastle by train.<br /> </p><br /> <br /> <p><br /> For information regarding accommodation will be available soon.<br /> <hr><br /> <br /> <h3 id="organisers">Organisers</h3><br /> <ul><br /> <li>[http://homepages.inf.ed.ac.uk/jeh/ Jane Hilston], University of Edinburgh</li><br /> <li>[http://www.dcs.gla.ac.uk/people/personal/gethin/ Gethin Norman], University of Glasgow</li><br /> </ul><br /> <br /> <hr><br /> <br /> <div id="abstracts"></div><br /> <h3 id="abstracts">Abstracts of Invited Talks</h3><br /> <br /> <ul><br /> <li>[http://cs.famaf.unc.edu.ar/~dargenio/ Pedro D'Argenio], FaMAF, Universidad Nacional de Cordoba<br /> <br><br /> Title: <em>Security analysis in probabilistic distributed protocols via bounded reachability.<br /> </em><br><br /> Abstract: Probabilistic model checking computes the probability values of a given property quantifying over all possible schedulers (also known as adversaries or policies). It turns out that maximum and minimum probabilities calculated in such a way are overestimations on models of distributed systems in which components are loosely coupled and share little information with each other. The problem exacerbates, if n addition the system is intended to protect private information.<br /> <br><br><br /> In this talk, we will (1) discuss the problem, (2) give a characterization for the set of schedulers that respect the distributed nature of process and the idea of secrecy, (3) report of some important properties of this class of schedulers, and (4) present an algorithm to analyze time-bounded reachability properties based on polynomial optimization. We will briefly discuss a prototype implementation and report some case studies.<br /> <br><br></li><br /> <li>[http://www.dsi.unive.it/~marin/ Andrea Marin], Universita di Venezia<br /> <br><br /> Title: <em>Compositional model specifications and analyses via product-forms</em><br><br /> Abstract: Compositionality is an important aspect of many formalisms used for<br /> quantitative analysis of computer software and hardware architectures<br /> and communication systems. Compositionality allows for the specification <br /> of complex models in terms of cooperations of simpler components in<br /> a modular and hierarchical way. <br /> However, these elegant and often compact model definitions often hide<br /> a huge complexity in the structure of the state space. For models with<br /> underlying continuous or discrete time Markov chains this implies that the quantitative<br /> evaluation of performance and reliability indices cannot rely on<br /> brute force approaches (such as the solution of the set of global balance<br /> equations). Therefore, from the point of view of the<br /> quantitative analysis of compositional models, an approach<br /> that allows one to tackle large state spaces is needed. When<br /> the models are characterised by underlying continuous time Markov<br /> chains (e.g., stochastic Petri nets, Performance Evaluation Process algebra -PEPA-) <br /> product-form theory may be successfully applied. Informally, product-forms<br /> aim at studying the model properties in steady-state starting from the<br /> analysis of its isolated components which are opportunely "parametrised" in order<br /> to take into account the interactions with the remaining parts of the model. <br /> <br><br><br /> After introducing product-form theory in stochastic process algebra<br /> domain, the talk will address the problem of deciding if product-form conditions<br /> are satisfied by the composition of a set of components and how the parameterisation<br /> of these components can be achieved. Special attention will be devoted to the<br /> automation of these steps even in cases of models with infinite state spaces.<br /> The Iterative Numerical Algorithm for Product-forms will be presented. <br /> Concluding remarks will consider the problem of the computation of the <br /> normalising constant and product-form approximations.<br /> <br><br><br /> </li><br /> <br /> <li>[http://www.pst.ifi.lmu.de/people/staff/tribastone/ Mirco Tribastone], Ludwig-Maximilians-Universit&#228;t M&#252;nchen <br /> <br><br /> Title: <em>Exact Aggregation for Fluid Process Algebra Models</em><br><br /> Abstract: Recent research in stochastic process algebra has led to efficient fluid approximation techniques obtained by aggregating large populations of sequential components into a single continuous-state variable represented as an ordinary differential equation (ODE). In this talk I will show that, when aggregation is performed higher up in the syntax tree of a model --- i.e., when one is interested in replicas of composite processes --- the resulting ODE system does not scale well with population sizes. I will present two techniques to tackle this problem. The first one is a model-to-model transformation at the process-algebra level. It converts a model with a large ODE system into another one whose size is independent from all population levels, but whose solution is related exactly to that of the original system. Simple syntactic checks are a necessary condition for this transformation to be carried out. The second technique enlarges the class of models amenable to exact aggregation. It performs a transformation directly at the level of the underlying ODE system, which is induced by a novel notion of behavioural equivalence for process algebra with fluid semantics. <br /> </li><br /> </ul></div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=File:Sicsa.jpg&diff=401 File:Sicsa.jpg 2012-06-24T16:20:27Z

<p>Ender: </p> <hr /> <div></div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=MLQA_2012&diff=400 MLQA 2012 2012-06-24T16:19:55Z

<p>Ender: </p> <hr /> <div><table width="100%" border="0"><br /> <tr><br /> <td><br /> <h1>Joint Workshop on Compositional Modelling and Analysis of Quantitative Systems</h1><br /> <h2>September 8, 2012</h2><br /> <h2>University of Edinburgh</h2><br /> </td><br /> <td>&nbsp;</td><br /> <td align="right"><br /> <table width="100%" border="0"><br /> <tr><br /> <td align="right"><br />  </td><br /> </tr></table><br /> <a href="http://www.sicsa.ac.uk/themes/modelling-and-abstraction" target="_blank"><img src="sicsa.jpg" alt="sicsa*" border="0" ></a></td><br /> </tr><br /> </table><br /> <br /> <hr><br /> <br /> <br /> <br /> <br /> <br /> <hr><br /> <br /> <h3 id="overview">Overview</h3><br /> <br /> <p><br /> The workshop combines the Fourth annual meeting of the [http://wiki.ercim.eu/wg/MLQA ERCIM Working Group on Models and Logics for Quantitative Analysis (MLQA)] with a [http://www.sicsa.ac.uk/themes/modelling-and-abstraction SICSA Modelling and Abstraction Theme] event.<br /> </p><br /> <br /> <p><br /> The theme of the workshop is <em>Compositional Modelling and Analysis of Quantitative Systems</em>. Compositionality is a key concept in both the modeling and analysis of computer systems. It is only by decomposing large complex system into smaller pieces, we can build and analyse these systems.<br /> </p><br /> <br /> <p><br /> The aim of the workshop is to bring together researchers working on quantitative modelling and analysis of computer systems focusing on research using compositional techniques. The workshop hopes to encourage interaction and collaboration between the attendees in developing compositional approaches. <br /> The workshop will bring together MLQA participants from across Europe with contributors to the SICSA theme of 'Modelling and Abstraction'. However, participation from outside MLQA and the SICSA theme are also welcome. <br /> </p><br /> <br /> <p><br /> The workshop will take place immediately following the [http://conferences.ncl.ac.uk/concur-2012/ CONCUR International Conference] taking place in Newcastle-upon-Tyne<br /> 4-7th September 2012.<br /> </p> <br /> <br /> <hr><br /> <br /> <h3 id="speakers">Invited speakers</h3> <br /> <br /> <ul><br /> <li>[http://cs.famaf.unc.edu.ar/~dargenio/ Pedro D'Argenio], FaMAF, Universidad Nacional de Cordoba<br /> <br><br /> <em>Security analysis in probabilistic distributed protocols via bounded reachability</em><br /> </li><br /> <li>[http://www.dsi.unive.it/~marin/ Andrea Marin], Universita di Venezia<br><br /> <em>Compositional model specifications and analyses via product-forms</em></li><br /> <li>[http://wwwhome.cs.utwente.nl/~vdpol/ Jaco van de Pol], University of Twente<br /> <br><br /> <em>tbc</em><br /> </li><br /> <li>[http://www.pst.ifi.lmu.de/people/staff/tribastone/ Mirco Tribastone], Ludwig-Maximilians-Universit&#228;t M&#252;nchen <br /> <br><br /> <em>Exact Aggregation for Fluid Process Algebra Models</em><br /> </li><br /> </ul><br /> <br /> <p><br /> Abstracts of the invited talks are available [[abstracts|here]].<br /> </p><br /> <br /> <hr><br /> <br /> <h3 id="registration">Registration</h3><br /> <br /> <p><br /> Registration will be at a cost of £25. Registration is free for members of SICSA institutions.<br /> </p><br /> <br /> <hr><br /> <br /> <h3 id="posters">Posters</h3><br /> <br /> <br /> <p><br /> We invited posters under two categories:<br /> </p><br /> <br /> <ul><li><br /> Presentation of recent or on-going work in relation to the themes of MLQA.<br /> </li><br /> <li><br /> Overview of the recent research activities of a research group related to the themes of MLQA.<br /> </li><br /> </ul><br /> <br /> <p><br /> We equally encourage submissions from both research leaders, junior researchers and PhD students.<br /> </p><br /> <br /> <p><br /> Posters should be printed by the <em>participants</em> in their preferred size.<br /> </p><br /> <br /> <p><br /> Notification of your intention to submit, along with a title and short description of the poster, should be sent by <b>August 31</b> to [mailto:gethin.norman@glasgow.ac.uk gethin.norman@glasgow.ac.uk].<br /> </p><br /> <br /> <hr><br /> <br /> <h3 id="programme">Preliminary Programme</h3><br /> <br /> <ul><br /> <li>09:30 - 09:45 <em>Opening</em><br /> </li><br /> <li>09:45 - 10:30 <em>invited talk</em><br /> <br><br><br /> </li><br /> <li>10:30 - 11:00 <em>coffee</em><br /> <br><br><br /> </li><br /> <li>11:00 - 11:45 <em>Invited talk</em><br /> </li><br /> <li>11:45 - 12:30 <em>Invited talk</em><br /> <br><br><br /> </li><br /> <li>12:30 - 14:00 <em>lunch & poster session</em><br /> <br><br><br /> </li><br /> <li>14:00 - 14:30 <em>SICSA Contributed talk</em><br /> </li><br /> <li>14:30 - 15:00 <em>SICSA Contributed talk</em><br /> </li><br /> <li>15:00 - 15:30 <em>SICSA Contributed talk</em><br /> <br><br><br /> </li><br /> <li>15:30 - 16:00 <em>coffee</em><br /> <br><br><br /> </li><br /> <li>16:00 - 17:00 <em>MLQA business meeting</em><br /> </li><br /> </ul><br /> <br /> <hr><br /> <br /> <h3 id="travel">Travel and Accommodation</h3><br /> <br /> <p><br /> The workshop will take place at the<br /> Informatics Forum of the School of Informatics, University of Edinburgh. For details on its location as well as links for travel directions see [http://www.ed.ac.uk/schools-departments/informatics/about/location here]. For those attending CONCUR, Edinburgh is approximately 90 minutes from Newcastle by train.<br /> </p><br /> <br /> <p><br /> For information regarding accommodation will be available soon.<br /> <hr><br /> <br /> <h3 id="organisers">Organisers</h3><br /> <ul><br /> <li>[http://homepages.inf.ed.ac.uk/jeh/ Jane Hilston], University of Edinburgh</li><br /> <li>[http://www.dcs.gla.ac.uk/people/personal/gethin/ Gethin Norman], University of Glasgow</li><br /> </ul><br /> <br /> <hr><br /> <br /> <div id="abstracts"></div><br /> <h3 id="abstracts">Abstracts of Invited Talks</h3><br /> <br /> <ul><br /> <li>[http://cs.famaf.unc.edu.ar/~dargenio/ Pedro D'Argenio], FaMAF, Universidad Nacional de Cordoba<br /> <br><br /> Title: <em>Security analysis in probabilistic distributed protocols via bounded reachability.<br /> </em><br><br /> Abstract: Probabilistic model checking computes the probability values of a given property quantifying over all possible schedulers (also known as adversaries or policies). It turns out that maximum and minimum probabilities calculated in such a way are overestimations on models of distributed systems in which components are loosely coupled and share little information with each other. The problem exacerbates, if n addition the system is intended to protect private information.<br /> <br><br><br /> In this talk, we will (1) discuss the problem, (2) give a characterization for the set of schedulers that respect the distributed nature of process and the idea of secrecy, (3) report of some important properties of this class of schedulers, and (4) present an algorithm to analyze time-bounded reachability properties based on polynomial optimization. We will briefly discuss a prototype implementation and report some case studies.<br /> <br><br></li><br /> <li>[http://www.dsi.unive.it/~marin/ Andrea Marin], Universita di Venezia<br /> <br><br /> Title: <em>Compositional model specifications and analyses via product-forms</em><br><br /> Abstract: Compositionality is an important aspect of many formalisms used for<br /> quantitative analysis of computer software and hardware architectures<br /> and communication systems. Compositionality allows for the specification <br /> of complex models in terms of cooperations of simpler components in<br /> a modular and hierarchical way. <br /> However, these elegant and often compact model definitions often hide<br /> a huge complexity in the structure of the state space. For models with<br /> underlying continuous or discrete time Markov chains this implies that the quantitative<br /> evaluation of performance and reliability indices cannot rely on<br /> brute force approaches (such as the solution of the set of global balance<br /> equations). Therefore, from the point of view of the<br /> quantitative analysis of compositional models, an approach<br /> that allows one to tackle large state spaces is needed. When<br /> the models are characterised by underlying continuous time Markov<br /> chains (e.g., stochastic Petri nets, Performance Evaluation Process algebra -PEPA-) <br /> product-form theory may be successfully applied. Informally, product-forms<br /> aim at studying the model properties in steady-state starting from the<br /> analysis of its isolated components which are opportunely "parametrised" in order<br /> to take into account the interactions with the remaining parts of the model. <br /> <br><br><br /> After introducing product-form theory in stochastic process algebra<br /> domain, the talk will address the problem of deciding if product-form conditions<br /> are satisfied by the composition of a set of components and how the parameterisation<br /> of these components can be achieved. Special attention will be devoted to the<br /> automation of these steps even in cases of models with infinite state spaces.<br /> The Iterative Numerical Algorithm for Product-forms will be presented. <br /> Concluding remarks will consider the problem of the computation of the <br /> normalising constant and product-form approximations.<br /> <br><br><br /> </li><br /> <br /> <li>[http://www.pst.ifi.lmu.de/people/staff/tribastone/ Mirco Tribastone], Ludwig-Maximilians-Universit&#228;t M&#252;nchen <br /> <br><br /> Title: <em>Exact Aggregation for Fluid Process Algebra Models</em><br><br /> Abstract: Recent research in stochastic process algebra has led to efficient fluid approximation techniques obtained by aggregating large populations of sequential components into a single continuous-state variable represented as an ordinary differential equation (ODE). In this talk I will show that, when aggregation is performed higher up in the syntax tree of a model --- i.e., when one is interested in replicas of composite processes --- the resulting ODE system does not scale well with population sizes. I will present two techniques to tackle this problem. The first one is a model-to-model transformation at the process-algebra level. It converts a model with a large ODE system into another one whose size is independent from all population levels, but whose solution is related exactly to that of the original system. Simple syntactic checks are a necessary condition for this transformation to be carried out. The second technique enlarges the class of models amenable to exact aggregation. It performs a transformation directly at the level of the underlying ODE system, which is induced by a novel notion of behavioural equivalence for process algebra with fluid semantics. <br /> </li><br /> </ul></div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=MLQA_2012&diff=399 MLQA 2012 2012-06-24T16:07:29Z

<p>Ender: </p> <hr /> <div><table width="100%" border="0"><br /> <tr><br /> <td><br /> <h1>Joint Workshop on Compositional Modelling and Analysis of Quantitative Systems</h1><br /> <h2>September 8, 2012</h2><br /> <h2>University of Edinburgh</h2><br /> </td><br /> <td>&nbsp;</td><br /> <td align="right"><br /> <table width="100%" border="0"><br /> <tr><br /> <td align="right"><br />  </td><br /> </tr></table><br /> <a href="http://www.sicsa.ac.uk/themes/modelling-and-abstraction" target="_blank"><img src="sicsa.jpg" alt="sicsa*" border="0" ></a></td><br /> </tr><br /> </table><br /> <br /> <hr><br /> <br /> <br /> <br /> <ul><br /> <li><a href="#overview">Overview</a><br /> <li><a href="#speakers">Invited Speakers</a><br /> <li><a href="#registration">Registration</a><br /> <li><a href="#posters">Posters</a><br /> <li><a href="#programme">Programme</a><br /> <li><a href="#travel">Travel and Accommodation</a><br /> <li><a href="#abstracts">Abstracts of Invited Talks</a><br /> </ul><br /> <br /> <hr><br /> <br /> <h3 id="overview">Overview</h3><br /> <br /> <p><br /> The workshop combines the Fourth annual meeting of the <a href="http://wiki.ercim.eu/wg/MLQA" target="_blank">ERCIM Working Group on Models and Logics for Quantitative Analysis (MLQA)</a> with a <a href="http://www.sicsa.ac.uk/themes/modelling-and-abstraction" target="_blank">SICSA Modelling and Abstraction Theme</a> event.<br /> </p><br /> <br /> <p><br /> The theme of the workshop is <em>Compositional Modelling and Analysis of Quantitative Systems</em>. Compositionality is a key concept in both the modeling and analysis of computer systems. It is only by decomposing large complex system into smaller pieces, we can build and analyse these systems.<br /> </p><br /> <br /> <p><br /> The aim of the workshop is to bring together researchers working on quantitative modelling and analysis of computer systems focusing on research using compositional techniques. The workshop hopes to encourage interaction and collaboration between the attendees in developing compositional approaches. <br /> The workshop will bring together MLQA participants from across Europe with contributors to the SICSA theme of 'Modelling and Abstraction'. However, participation from outside MLQA and the SICSA theme are also welcome. <br /> </p><br /> <br /> <p><br /> The workshop will take place immediately following the <a href="http://conferences.ncl.ac.uk/concur-2012/" target="_blank">CONCUR International Conference</a> taking place in Newcastle-upon-Tyne<br /> 4-7th September 2012.<br /> </p> <br /> <br /> <hr><br /> <br /> <h3 id="speakers">Invited speakers</h3> <br /> <br /> <ul><br /> <li>[http://cs.famaf.unc.edu.ar/~dargenio/ Pedro D'Argenio], FaMAF, Universidad Nacional de Cordoba<br /> <br><br /> <em>Security analysis in probabilistic distributed protocols via bounded reachability</em><br /> </li><br /> <li>[http://www.dsi.unive.it/~marin/ Andrea Marin], Universita di Venezia<br><br /> <em>Compositional model specifications and analyses via product-forms</em></li><br /> <li>[http://wwwhome.cs.utwente.nl/~vdpol/ Jaco van de Pol], University of Twente<br /> <br><br /> <em>tbc</em><br /> </li><br /> <li>[http://www.pst.ifi.lmu.de/people/staff/tribastone/ Mirco Tribastone], Ludwig-Maximilians-Universit&#228;t M&#252;nchen <br /> <br><br /> <em>Exact Aggregation for Fluid Process Algebra Models</em><br /> </li><br /> </ul><br /> <br /> <p><br /> Abstracts of the invited talks are available <a href="#abstracts">here</a>.<br /> </p><br /> <br /> <hr><br /> <br /> <h3 id="registration">Registration</h3><br /> <br /> <p><br /> Registration will be at a cost of £25. Registration is free for members of SICSA institutions.<br /> </p><br /> <br /> <hr><br /> <br /> <h3 id="posters">Posters</h3><br /> <br /> <br /> <p><br /> We invited posters under two categories:<br /> </p><br /> <br /> <ul><li><br /> Presentation of recent or on-going work in relation to the themes of MLQA.<br /> </li><br /> <li><br /> Overview of the recent research activities of a research group related to the themes of MLQA.<br /> </li><br /> </ul><br /> <br /> <p><br /> We equally encourage submissions from both research leaders, junior researchers and PhD students.<br /> </p><br /> <br /> <p><br /> Posters should be printed by the <em>participants</em> in their preferred size.<br /> </p><br /> <br /> <p><br /> Notification of your intention to submit, along with a title and short description of the poster, should be sent by <b>August 31</b> to [mailto:gethin.norman@glasgow.ac.uk gethin.norman@glasgow.ac.uk].<br /> </p><br /> <br /> <hr><br /> <br /> <h3 id="programme">Preliminary Programme</h3><br /> <br /> <ul><br /> <li>09:30 - 09:45 <em>Opening</em><br /> </li><br /> <li>09:45 - 10:30 <em>invited talk</em><br /> <br><br><br /> </li><br /> <li>10:30 - 11:00 <em>coffee</em><br /> <br><br><br /> </li><br /> <li>11:00 - 11:45 <em>Invited talk</em><br /> </li><br /> <li>11:45 - 12:30 <em>Invited talk</em><br /> <br><br><br /> </li><br /> <li>12:30 - 14:00 <em>lunch & poster session</em><br /> <br><br><br /> </li><br /> <li>14:00 - 14:30 <em>SICSA Contributed talk</em><br /> </li><br /> <li>14:30 - 15:00 <em>SICSA Contributed talk</em><br /> </li><br /> <li>15:00 - 15:30 <em>SICSA Contributed talk</em><br /> <br><br><br /> </li><br /> <li>15:30 - 16:00 <em>coffee</em><br /> <br><br><br /> </li><br /> <li>16:00 - 17:00 <em>MLQA business meeting</em><br /> </li><br /> </ul><br /> <br /> <hr><br /> <br /> <h3 id="travel">Travel and Accommodation</h3><br /> <br /> <p><br /> The workshop will take place at the<br /> Informatics Forum of the School of Informatics, University of Edinburgh. For details on its location as well as links for travel directions see [http://www.ed.ac.uk/schools-departments/informatics/about/location here]. For those attending CONCUR, Edinburgh is approximately 90 minutes from Newcastle by train.<br /> </p><br /> <br /> <p><br /> For information regarding accommodation will be available soon.<br /> <hr><br /> <br /> <h3 id="organisers">Organisers</h3><br /> <ul><br /> <li>[http://homepages.inf.ed.ac.uk/jeh/ Jane Hilston], University of Edinburgh</li><br /> <li>[http://www.dcs.gla.ac.uk/people/personal/gethin/ Gethin Norman], University of Glasgow</li><br /> </ul><br /> <br /> <hr><br /> <br /> <h3 id="abstracts">Abstracts of Invited Talks</h3><br /> <br /> <ul><br /> <li>[http://cs.famaf.unc.edu.ar/~dargenio/ Pedro D'Argenio], FaMAF, Universidad Nacional de Cordoba<br /> <br><br /> Title: <em>Security analysis in probabilistic distributed protocols via bounded reachability.<br /> </em><br><br /> Abstract: Probabilistic model checking computes the probability values of a given property quantifying over all possible schedulers (also known as adversaries or policies). It turns out that maximum and minimum probabilities calculated in such a way are overestimations on models of distributed systems in which components are loosely coupled and share little information with each other. The problem exacerbates, if n addition the system is intended to protect private information.<br /> <br><br><br /> In this talk, we will (1) discuss the problem, (2) give a characterization for the set of schedulers that respect the distributed nature of process and the idea of secrecy, (3) report of some important properties of this class of schedulers, and (4) present an algorithm to analyze time-bounded reachability properties based on polynomial optimization. We will briefly discuss a prototype implementation and report some case studies.<br /> <br><br></li><br /> <li>[http://www.dsi.unive.it/~marin/ Andrea Marin], Universita di Venezia<br /> <br><br /> Title: <em>Compositional model specifications and analyses via product-forms</em><br><br /> Abstract: Compositionality is an important aspect of many formalisms used for<br /> quantitative analysis of computer software and hardware architectures<br /> and communication systems. Compositionality allows for the specification <br /> of complex models in terms of cooperations of simpler components in<br /> a modular and hierarchical way. <br /> However, these elegant and often compact model definitions often hide<br /> a huge complexity in the structure of the state space. For models with<br /> underlying continuous or discrete time Markov chains this implies that the quantitative<br /> evaluation of performance and reliability indices cannot rely on<br /> brute force approaches (such as the solution of the set of global balance<br /> equations). Therefore, from the point of view of the<br /> quantitative analysis of compositional models, an approach<br /> that allows one to tackle large state spaces is needed. When<br /> the models are characterised by underlying continuous time Markov<br /> chains (e.g., stochastic Petri nets, Performance Evaluation Process algebra -PEPA-) <br /> product-form theory may be successfully applied. Informally, product-forms<br /> aim at studying the model properties in steady-state starting from the<br /> analysis of its isolated components which are opportunely "parametrised" in order<br /> to take into account the interactions with the remaining parts of the model. <br /> <br><br><br /> After introducing product-form theory in stochastic process algebra<br /> domain, the talk will address the problem of deciding if product-form conditions<br /> are satisfied by the composition of a set of components and how the parameterisation<br /> of these components can be achieved. Special attention will be devoted to the<br /> automation of these steps even in cases of models with infinite state spaces.<br /> The Iterative Numerical Algorithm for Product-forms will be presented. <br /> Concluding remarks will consider the problem of the computation of the <br /> normalising constant and product-form approximations.<br /> <br><br><br /> </li><br /> <br /> <li>[http://www.pst.ifi.lmu.de/people/staff/tribastone/ Mirco Tribastone], Ludwig-Maximilians-Universit&#228;t M&#252;nchen <br /> <br><br /> Title: <em>Exact Aggregation for Fluid Process Algebra Models</em><br><br /> Abstract: Recent research in stochastic process algebra has led to efficient fluid approximation techniques obtained by aggregating large populations of sequential components into a single continuous-state variable represented as an ordinary differential equation (ODE). In this talk I will show that, when aggregation is performed higher up in the syntax tree of a model --- i.e., when one is interested in replicas of composite processes --- the resulting ODE system does not scale well with population sizes. I will present two techniques to tackle this problem. The first one is a model-to-model transformation at the process-algebra level. It converts a model with a large ODE system into another one whose size is independent from all population levels, but whose solution is related exactly to that of the original system. Simple syntactic checks are a necessary condition for this transformation to be carried out. The second technique enlarges the class of models amenable to exact aggregation. It performs a transformation directly at the level of the underlying ODE system, which is induced by a novel notion of behavioural equivalence for process algebra with fluid semantics. <br /> </li><br /> </ul></div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=Main_Page&diff=398 Main Page 2012-06-24T15:51:12Z

<p>Ender: /* Upcoming events */</p> <hr /> <div>== ERCIM Working Group on Models and Logics for Quantitative Analysis (MLQA) ==<br /> <br /> [[Image:Image002.png|frame]] Models and Logics for Quantitative Analysis are seen as comprising process models analysed using logics for quantitative properties. More specifically, we will<br /> <br /> # consider process models formally described by transition systems, automata or process calculi,<br /> # consider logics for expressing stochastic and continuous properties as well as discrete ones,<br /> # focus on algorithms, theory and tools, and<br /> # study applications with particular emphasis on embedded systems and service oriented systems but will aim at treating also IT guided workflow systems and biological systems.<br /> <br /> The MLQA home page: http://wiki.ercim.eu/wg/MLQA<br /> <br /> The goal of this working group is to create a venue for knowledge sharing in this exciting area, for creating a network also for young researchers, for sharing tools developed within the field, for discussing research directions, and eventually to formulate a European project or network on formal quantitative analysis.<br /> <br /> The working group will be open also to researchers outside of ERCIM (and outside of Europe).<br /> <br /> == Upcoming events ==<br /> <br /> The fourth annual meeting: [[MLQA 2012]], Edinburgh, UK.<br /> <br /> The fifth annual meeting: [[MLQA 2013]], Rome, Italy.<br /> <br /> == Past events ==<br /> <br /> The Kick-Off meeting: [[MLQA 2009|MLQA 2009]], York, UK.<br /> <br /> The second annual meeting: [[MLQA 2010|MLQA 2010]], Edinburgh, UK.<br /> <br /> The third annual meeting: [[MLQA 2011|MLQA 2011]], Aachen, Germany.</div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=Main_Page&diff=397 Main Page 2012-06-24T15:42:25Z

<p>Ender: /* Past events */</p> <hr /> <div>== ERCIM Working Group on Models and Logics for Quantitative Analysis (MLQA) ==<br /> <br /> [[Image:Image002.png|frame]] Models and Logics for Quantitative Analysis are seen as comprising process models analysed using logics for quantitative properties. More specifically, we will<br /> <br /> # consider process models formally described by transition systems, automata or process calculi,<br /> # consider logics for expressing stochastic and continuous properties as well as discrete ones,<br /> # focus on algorithms, theory and tools, and<br /> # study applications with particular emphasis on embedded systems and service oriented systems but will aim at treating also IT guided workflow systems and biological systems.<br /> <br /> The MLQA home page: http://wiki.ercim.eu/wg/MLQA<br /> <br /> The goal of this working group is to create a venue for knowledge sharing in this exciting area, for creating a network also for young researchers, for sharing tools developed within the field, for discussing research directions, and eventually to formulate a European project or network on formal quantitative analysis.<br /> <br /> The working group will be open also to researchers outside of ERCIM (and outside of Europe).<br /> <br /> == Upcoming events ==<br /> <br /> The fourth annual meeting: [[MLQA 2012]]<br /> <br /> The fifth annual meeting: [[MLQA 2013]]<br /> <br /> == Past events ==<br /> <br /> The Kick-Off meeting: [[MLQA 2009|MLQA 2009]], York, UK.<br /> <br /> The second annual meeting: [[MLQA 2010|MLQA 2010]], Edinburgh, UK.<br /> <br /> The third annual meeting: [[MLQA 2011|MLQA 2011]], Aachen, Germany.</div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=MLQA_2012&diff=396 MLQA 2012 2012-01-24T12:49:58Z

<p>Ender: New page: The fourth annual meeting of the MLQA working group, MLQA 2012, will take place in Edinburgh on Saturday 8 September 2012. The details of the meeting will be posted on this page soon.</p> <hr /> <div>The fourth annual meeting of the MLQA working group, MLQA 2012, will take place in Edinburgh on Saturday 8 September 2012. The details of the meeting will be posted on this page soon.</div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=MLQA_2013&diff=395 MLQA 2013 2012-01-24T12:47:30Z

<p>Ender: </p> <hr /> <div>The fifth annual meeting of the MLQA working group will take place on Sunday 24 March 2013 as part of the European Joint Conferences on Theory And Practice of Software (ETAPS) in Rome, Italy. The details of the meeting will be posted on this page soon.</div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=Main_Page&diff=394 Main Page 2012-01-24T12:46:23Z

<p>Ender: </p> <hr /> <div>== ERCIM Working Group on Models and Logics for Quantitative Analysis (MLQA) ==<br /> <br /> [[Image:Image002.png|frame]] Models and Logics for Quantitative Analysis are seen as comprising process models analysed using logics for quantitative properties. More specifically, we will<br /> <br /> # consider process models formally described by transition systems, automata or process calculi,<br /> # consider logics for expressing stochastic and continuous properties as well as discrete ones,<br /> # focus on algorithms, theory and tools, and<br /> # study applications with particular emphasis on embedded systems and service oriented systems but will aim at treating also IT guided workflow systems and biological systems.<br /> <br /> The MLQA home page: http://wiki.ercim.eu/wg/MLQA<br /> <br /> The goal of this working group is to create a venue for knowledge sharing in this exciting area, for creating a network also for young researchers, for sharing tools developed within the field, for discussing research directions, and eventually to formulate a European project or network on formal quantitative analysis.<br /> <br /> The working group will be open also to researchers outside of ERCIM (and outside of Europe).<br /> <br /> == Upcoming events ==<br /> <br /> The fourth annual meeting: [[MLQA 2012]]<br /> <br /> The fifth annual meeting: [[MLQA 2013]]<br /> <br /> == Past events ==<br /> <br /> The Kick-Off meeting: [[MLQA 2009|MLQA 2009]]<br /> <br /> The second annual meeting: [[MLQA 2010|MLQA 2010]]<br /> <br /> The third annual meeting: [[MLQA 2011|MLQA 2011]]</div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=Main_Page&diff=393 Main Page 2012-01-13T09:56:04Z

<p>Ender: /* Upcoming events */</p> <hr /> <div>== ERCIM Working Group on Models and Logics for Quantitative Analysis (MLQA) ==<br /> <br /> [[Image:Image002.png|frame]] Models and Logics for Quantitative Analysis are seen as comprising process models analysed using logics for quantitative properties. More specifically, we will<br /> <br /> # consider process models formally described by transition systems, automata or process calculi,<br /> # consider logics for expressing stochastic and continuous properties as well as discrete ones,<br /> # focus on algorithms, theory and tools, and<br /> # study applications with particular emphasis on embedded systems and service oriented systems but will aim at treating also IT guided workflow systems and biological systems.<br /> <br /> The MLQA home page: http://wiki.ercim.eu/wg/MLQA<br /> <br /> The goal of this working group is to create a venue for knowledge sharing in this exciting area, for creating a network also for young researchers, for sharing tools developed within the field, for discussing research directions, and eventually to formulate a European project or network on formal quantitative analysis.<br /> <br /> The working group will be open also to researchers outside of ERCIM (and outside of Europe).<br /> <br /> == Upcoming events ==<br /> <br /> The fourth annual meeting: [[MLQA 2013]]<br /> <br /> == Past events ==<br /> <br /> The Kick-Off meeting: [[MLQA 2009|MLQA 2009]]<br /> <br /> The second annual meeting: [[MLQA 2010|MLQA 2010]]<br /> <br /> The third annual meeting: [[MLQA 2011|MLQA 2011]]</div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=Main_Page&diff=392 Main Page 2012-01-13T09:55:55Z

<p>Ender: /* Upcoming events */</p> <hr /> <div>== ERCIM Working Group on Models and Logics for Quantitative Analysis (MLQA) ==<br /> <br /> [[Image:Image002.png|frame]] Models and Logics for Quantitative Analysis are seen as comprising process models analysed using logics for quantitative properties. More specifically, we will<br /> <br /> # consider process models formally described by transition systems, automata or process calculi,<br /> # consider logics for expressing stochastic and continuous properties as well as discrete ones,<br /> # focus on algorithms, theory and tools, and<br /> # study applications with particular emphasis on embedded systems and service oriented systems but will aim at treating also IT guided workflow systems and biological systems.<br /> <br /> The MLQA home page: http://wiki.ercim.eu/wg/MLQA<br /> <br /> The goal of this working group is to create a venue for knowledge sharing in this exciting area, for creating a network also for young researchers, for sharing tools developed within the field, for discussing research directions, and eventually to formulate a European project or network on formal quantitative analysis.<br /> <br /> The working group will be open also to researchers outside of ERCIM (and outside of Europe).<br /> <br /> == Upcoming events ==<br /> <br /> The third annual meeting: [[MLQA 2013]]<br /> <br /> == Past events ==<br /> <br /> The Kick-Off meeting: [[MLQA 2009|MLQA 2009]]<br /> <br /> The second annual meeting: [[MLQA 2010|MLQA 2010]]<br /> <br /> The third annual meeting: [[MLQA 2011|MLQA 2011]]</div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=MLQA_2013&diff=391 MLQA 2013 2012-01-13T09:55:23Z

<p>Ender: New page: The fourth annual meeting of the MLQA working group will take place on Sunday 24 March 2013 as part of the European Joint Conferences on Theory And Practice of Software (ETAPS) in Rome, It...</p> <hr /> <div>The fourth annual meeting of the MLQA working group will take place on Sunday 24 March 2013 as part of the European Joint Conferences on Theory And Practice of Software (ETAPS) in Rome, Italy. The details of the meeting will be posted on this page soon.</div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=Main_Page&diff=390 Main Page 2012-01-13T09:49:43Z

<p>Ender: /* Past events */</p> <hr /> <div>== ERCIM Working Group on Models and Logics for Quantitative Analysis (MLQA) ==<br /> <br /> [[Image:Image002.png|frame]] Models and Logics for Quantitative Analysis are seen as comprising process models analysed using logics for quantitative properties. More specifically, we will<br /> <br /> # consider process models formally described by transition systems, automata or process calculi,<br /> # consider logics for expressing stochastic and continuous properties as well as discrete ones,<br /> # focus on algorithms, theory and tools, and<br /> # study applications with particular emphasis on embedded systems and service oriented systems but will aim at treating also IT guided workflow systems and biological systems.<br /> <br /> The MLQA home page: http://wiki.ercim.eu/wg/MLQA<br /> <br /> The goal of this working group is to create a venue for knowledge sharing in this exciting area, for creating a network also for young researchers, for sharing tools developed within the field, for discussing research directions, and eventually to formulate a European project or network on formal quantitative analysis.<br /> <br /> The working group will be open also to researchers outside of ERCIM (and outside of Europe).<br /> <br /> == Upcoming events ==<br /> <br /> [[MLQA 2013]]<br /> <br /> == Past events ==<br /> <br /> The Kick-Off meeting: [[MLQA 2009|MLQA 2009]]<br /> <br /> The second annual meeting: [[MLQA 2010|MLQA 2010]]<br /> <br /> The third annual meeting: [[MLQA 2011|MLQA 2011]]</div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=Main_Page&diff=389 Main Page 2012-01-13T09:48:46Z

<p>Ender: /* Upcoming events */</p> <hr /> <div>== ERCIM Working Group on Models and Logics for Quantitative Analysis (MLQA) ==<br /> <br /> [[Image:Image002.png|frame]] Models and Logics for Quantitative Analysis are seen as comprising process models analysed using logics for quantitative properties. More specifically, we will<br /> <br /> # consider process models formally described by transition systems, automata or process calculi,<br /> # consider logics for expressing stochastic and continuous properties as well as discrete ones,<br /> # focus on algorithms, theory and tools, and<br /> # study applications with particular emphasis on embedded systems and service oriented systems but will aim at treating also IT guided workflow systems and biological systems.<br /> <br /> The MLQA home page: http://wiki.ercim.eu/wg/MLQA<br /> <br /> The goal of this working group is to create a venue for knowledge sharing in this exciting area, for creating a network also for young researchers, for sharing tools developed within the field, for discussing research directions, and eventually to formulate a European project or network on formal quantitative analysis.<br /> <br /> The working group will be open also to researchers outside of ERCIM (and outside of Europe).<br /> <br /> == Upcoming events ==<br /> <br /> [[MLQA 2013]]<br /> <br /> == Past events ==<br /> <br /> [[MLQA 2009|MLQA 2009]]<br /> <br /> [[MLQA 2010|MLQA 2010]]<br /> <br /> [[MLQA 2011|MLQA 2011]]</div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=Main_Page&diff=388 Main Page 2012-01-13T09:47:36Z

<p>Ender: /* Upcoming events */</p> <hr /> <div>== ERCIM Working Group on Models and Logics for Quantitative Analysis (MLQA) ==<br /> <br /> [[Image:Image002.png|frame]] Models and Logics for Quantitative Analysis are seen as comprising process models analysed using logics for quantitative properties. More specifically, we will<br /> <br /> # consider process models formally described by transition systems, automata or process calculi,<br /> # consider logics for expressing stochastic and continuous properties as well as discrete ones,<br /> # focus on algorithms, theory and tools, and<br /> # study applications with particular emphasis on embedded systems and service oriented systems but will aim at treating also IT guided workflow systems and biological systems.<br /> <br /> The MLQA home page: http://wiki.ercim.eu/wg/MLQA<br /> <br /> The goal of this working group is to create a venue for knowledge sharing in this exciting area, for creating a network also for young researchers, for sharing tools developed within the field, for discussing research directions, and eventually to formulate a European project or network on formal quantitative analysis.<br /> <br /> The working group will be open also to researchers outside of ERCIM (and outside of Europe).<br /> <br /> == Upcoming events ==<br /> <br /> [[MLQA 2013]]: TBA.<br /> <br /> == Past events ==<br /> <br /> [[MLQA 2009|MLQA 2009]]<br /> <br /> [[MLQA 2010|MLQA 2010]]<br /> <br /> [[MLQA 2011|MLQA 2011]]</div>

Ender https://wiki.ercim.eu/wg/MLQA/index.php?title=MLQA_2011&diff=387 MLQA 2011 2011-09-12T15:59:12Z

<p>Ender: </p> <hr /> <div>The third annual meeting of the MLQA working group took place on September 5, 2011 in Aachen - colocated with CONCUR and QEST. The event consisted of a number of invited talks, a poster session and a business meeting. <br /> <br /> --------------- <br /> <br /> '''Programme'''<br /> <br /> The abstracts and the presentations of the talks in MLQA 2011 are available, please click on the titles below. <br /> <br /> '''Sept. 5, 2011'''<br /> <br /> * 09:30 - 09:45 [http://wiki.ercim.eu/wg/MLQA/images/d/d5/MLQA_2011-Welcome.pdf Opening]<br /> <br /> * 09:45 - 10:30 J.Y. Le Boudec, [[Abstracts MLQA 2011#ODEs and discrete simulation|ODEs and discrete simulation]]<br /> <br /> * 10:30 - 11:00 Cofee Break<br /> <br /> * 11:00 - 11:45 J. Hillston, [[Abstracts MLQA 2011#Stochastic process algebras and ODEs|Stochastic process algebras and ODEs]]<br /> <br /> * 11:45 - 12:30 L. Bortolussi, [[Abstracts MLQA 2011#On the Relationship between ODE, Simulation and Stochastic Process Algebras|On the Relationship between ODE, Simulation and Stochastic Process Algebras]]<br /> <br /> * 12:30 - 14:00 Lunch & poster session<br /> <br /> * 14:00 - 14:45 V. Wolf, [[Abstracts MLQA 2011#Stochastic Hybrid Analysis of Markov Population Models|Stochastic Hybrid Analysis of Markov Population Models]]<br /> <br /> * 14:45 - 15:30 J. Desharnais, [[Abstracts MLQA 2011#Approximation of continuous space systems and associated metrics and logics|Approximation of continuous space systems and associated metrics and logics]]<br /> <br /> * 15:30 - 16:00 Cofee Break<br /> <br /> * 16:00 - 17:00 [http://wiki.ercim.eu/wg/MLQA/images/1/17/MLQA_2011-Business.pdf MLQA business meeting]<br /> <br /> * 17:00 - 18:00 Thematic Small Working Group: [[Abstracts MLQA 2011#Small Thematic Working Group on Hidden Markov Models|Hidden Markov Chains and the languages/logics]]. Convened by Flemming Nielson<br /> <br /> <br /> See the [http://wiki.ercim.eu/wg/MLQA/images/c/c9/Minutes_from_the_MLQA_2011_Meeting.pdf minutes from the MLQA 2011 Meeting]</div>

Ender