Poster Session at MLQA 2010 - Revision history

Nataliya at 12:21, 20 July 2010

2010-07-20T12:21:19Z

← Older revision		Revision as of 12:21, 20 July 2010
Line 194:		Line 194:
	about simulated environments.		about simulated environments.

	Go back to [[~~July 2010:~~ MLQA ~~meeting at FLoC~~ 2010~~, Edinburgh~~\|MLQA meeting at FLoC 2010]]		Go back to [[MLQA 2010\|MLQA meeting at FLoC 2010]]

Nataliya at 12:19, 20 July 2010

2010-07-20T12:19:17Z

← Older revision		Revision as of 12:19, 20 July 2010
Line 193:		Line 193:
	the calculus and the BioShape tool to work in synergy towards the gaining of quantitative information		the calculus and the BioShape tool to work in synergy towards the gaining of quantitative information
	about simulated environments.		about simulated environments.

			Go back to [[July 2010: MLQA meeting at FLoC 2010, Edinburgh\|MLQA meeting at FLoC 2010]]

Nataliya at 13:27, 16 July 2010

2010-07-16T13:27:58Z

← Older revision		Revision as of 13:27, 16 July 2010
Line 22:		Line 22:
	Proceedings of QEST 2010.		Proceedings of QEST 2010.

	== Nataliya Skrypnyuk, Michael Smith. [http://wiki.ercim.eu/wg/MLQA/images/b/b2/Submission_2.pdf ~~Abstraction~~ of Stochastic Process Algebras.] ==		== Nataliya Skrypnyuk, Michael Smith. [http://wiki.ercim.eu/wg/MLQA/images/b/b2/Submission_2.pdf Abstractions of Stochastic Process Algebras.] ==

	Stochastic process algebras are compositional modelling languages		Stochastic process algebras are compositional modelling languages

Nataliya at 13:26, 16 July 2010

2010-07-16T13:26:35Z

← Older revision		Revision as of 13:26, 16 July 2010
Line 8:		Line 8:
	There were 11 poster submissions to the MLQA poster session. Click on a poster title in order to access the correspondent poster submission in the pdf format.		There were 11 poster submissions to the MLQA poster session. Click on a poster title in order to access the correspondent poster submission in the pdf format.

	===Michael Huth, Nir Piterman, Daniel Wagner. [http://wiki.ercim.eu/wg/MLQA/images/1/14/Submission_1.pdf p-Automata Approach to Probabilistic Verification].===		==Michael Huth, Nir Piterman, Daniel Wagner. [http://wiki.ercim.eu/wg/MLQA/images/1/14/Submission_1.pdf p-Automata Approach to Probabilistic Verification].==

	The poster introduces an automata based approach to the		The poster introduces an automata based approach to the
Line 22:		Line 22:
	Proceedings of QEST 2010.		Proceedings of QEST 2010.

	=== Nataliya Skrypnyuk, Michael Smith. Abstraction of Stochastic Process Algebras. ===		== Nataliya Skrypnyuk, Michael Smith. [http://wiki.ercim.eu/wg/MLQA/images/b/b2/Submission_2.pdf Abstraction of Stochastic Process Algebras.] ==

	Stochastic process algebras are compositional modelling languages		Stochastic process algebras are compositional modelling languages
Line 43:		Line 43:
	of PEPA using compositional aggregation of states.		of PEPA using compositional aggregation of states.

	=== Igor Cappello and Paola Quaglia. Quantitative Assessment of Web Services: Applying SCOWS to a Real-Life Scenario. ===		== Igor Cappello and Paola Quaglia. [http://wiki.ercim.eu/wg/MLQA/images/c/cb/Submission_3.pdf Quantitative Assessment of Web Services: Applying SCOWS to a Real-Life Scenario]. ==

	We present an example of application of SCOWS to a real-life scenario		We present an example of application of SCOWS to a real-life scenario
Line 63:		Line 63:
	the overall performance of the service.		the overall performance of the service.

	=== Ender Yüksel, Hanne Riis Nielson, and Flemming Nielson. High Security at a Low Cost. ===		== Ender Yüksel, Hanne Riis Nielson, and Flemming Nielson. [http://wiki.ercim.eu/wg/MLQA/images/4/44/Submission_4.pdf High Security at a Low Cost]. ==

	In the future tiny devices with microcontrollers and sensors will be in charge		In the future tiny devices with microcontrollers and sensors will be in charge
Line 86:		Line 86:
	on its behaviour. The properties we are interested in are expressed in continuous stochastic logic, and probabilistic model checker Prism is used in the analysis.		on its behaviour. The properties we are interested in are expressed in continuous stochastic logic, and probabilistic model checker Prism is used in the analysis.

	=== Erik de Vink, Suzana Andova, and Luuk Groenewegen. Towards Dynamic Adaptation of Probabilistic Systems. ===		== Erik de Vink, Suzana Andova, and Luuk Groenewegen. [http://wiki.ercim.eu/wg/MLQA/images/8/84/Submission_5.pdf Towards Dynamic Adaptation of Probabilistic Systems]. ==

	Dynamic system adaptation is modeled in Paradigm as coordination of		Dynamic system adaptation is modeled in Paradigm as coordination of
Line 100:		Line 100:
	system during adaptation.		system during adaptation.

	=== Fuyuan Zhang and Piotr Filipiuk. Model Checking is Static Analysis. ===		== Fuyuan Zhang and Piotr Filipiuk. [http://wiki.ercim.eu/wg/MLQA/images/5/5c/Submission_6.pdf Model Checking is Static Analysis]. ==

	The link between model checking and static analysis has been of great interest		The link between model checking and static analysis has been of great interest
Line 110:		Line 110:
	state-of-the-art approach to static analysis that bridges the gap between a number of approaches to static analysis including Data Flow Analysis, Constraint Based Analysis, Abstract Interpretation and Type and Effect Systems. In the developments it has been demonstrated that Flow Logic is a robust approach that is able to deal with a variety of calculi, programming languages and recently modal logics such as CTL, ACTL and alternation-free mu-calculus. In order to calculate the analysis solution, we use ALFP Suite that computes the least model guaranteed by the Moore family theorem for ALFP. In its current version, the suite supports two solvers, one being a differential worklist solver that is based on a representation of relations as prefix trees and the other being a solver in continuation passing style that is based on a BDD representation of relations.		state-of-the-art approach to static analysis that bridges the gap between a number of approaches to static analysis including Data Flow Analysis, Constraint Based Analysis, Abstract Interpretation and Type and Effect Systems. In the developments it has been demonstrated that Flow Logic is a robust approach that is able to deal with a variety of calculi, programming languages and recently modal logics such as CTL, ACTL and alternation-free mu-calculus. In order to calculate the analysis solution, we use ALFP Suite that computes the least model guaranteed by the Moore family theorem for ALFP. In its current version, the suite supports two solvers, one being a differential worklist solver that is based on a representation of relations as prefix trees and the other being a solver in continuation passing style that is based on a BDD representation of relations.

	=== Vashti Galpin, Jane Hillston, and Luca Bortolussi. A Stochastic Hybrid Process Algebra. ===		== Vashti Galpin, Jane Hillston, and Luca Bortolussi. [http://wiki.ercim.eu/wg/MLQA/images/8/83/Submission_7.pdf A Stochastic Hybrid Process Algebra]. ==

	The process algebra HYPE was developed to model hybrid systems which are		The process algebra HYPE was developed to model hybrid systems which are
Line 121:		Line 121:
	the evolution of the example over time based on stochastic simulation.		the evolution of the example over time based on stochastic simulation.

	=== David Cachera, Thomas Jensen, Arnaud Jobin, and Pascal Sotin. A Linear Operator Framework for Analysing Resource Usage. ===		== David Cachera, Thomas Jensen, Arnaud Jobin, and Pascal Sotin. [http://wiki.ercim.eu/wg/MLQA/images/1/12/Submission_8.pdf A Linear Operator Framework for Analysing Resource Usage]. ==

	We present a semantics-based framework for analysing the quantitative		We present a semantics-based framework for analysing the quantitative
Line 140:		Line 140:
	explicit energy modes management.		explicit energy modes management.

	=== Christoffer Sloth and Rafael Wisniewski. Verification of Continuous Dynamical Systems by Timed Automata. ===		== Christoffer Sloth and Rafael Wisniewski. [http://wiki.ercim.eu/wg/MLQA/images/e/eb/Submission_9.pdf Verification of Continuous Dynamical Systems by Timed Automata]. ==

	The poster outlines a method for abstracting continuous dynamical systems by finite		The poster outlines a method for abstracting continuous dynamical systems by finite
Line 164:		Line 164:
	complete abstractions are generated.		complete abstractions are generated.

	=== Lei Song, Flemming Nielson, and Bo Friis Nielson. A Broadcast Based Stochastic Calculus. ===		== Lei Song, Flemming Nielson, and Bo Friis Nielson. [http://wiki.ercim.eu/wg/MLQA/images/9/94/Submission_10.pdf A Broadcast Based Stochastic Calculus]. ==

	In our current work we give a stochastic calculus based on broadcast communication. Only		In our current work we give a stochastic calculus based on broadcast communication. Only
Line 174:		Line 174:
	process (BMAP), marked markovian arrival process (MMAP) and closed queueing networks.		process (BMAP), marked markovian arrival process (MMAP) and closed queueing networks.

	=== Massimo Callisto De Donato, Flavio Corradini, Maria Rita Di Berardini, Emanuela Merelli, and Luca Tesei. Tailoring the Shape Calculus for Quantitative Analysis. ===		== Massimo Callisto De Donato, Flavio Corradini, Maria Rita Di Berardini, Emanuela Merelli, and Luca Tesei. [http://wiki.ercim.eu/wg/MLQA/images/0/00/Submission_11.pdf Tailoring the Shape Calculus for Quantitative Analysis]. ==

	The Shape Calculus, a bio-inspired language, is a non-deterministic calculus in which processes		The Shape Calculus, a bio-inspired language, is a non-deterministic calculus in which processes

Nataliya at 13:07, 16 July 2010

2010-07-16T13:07:48Z

← Older revision		Revision as of 13:07, 16 July 2010
Line 8:		Line 8:
	There were 11 poster submissions to the MLQA poster session. Click on a poster title in order to access the correspondent poster submission in the pdf format.		There were 11 poster submissions to the MLQA poster session. Click on a poster title in order to access the correspondent poster submission in the pdf format.

	===Michael Huth, Nir Piterman, Daniel Wagner. [http://wiki.ercim.eu/wg/MLQA/~~index.php~~/~~Image:~~Submission_1.pdf p-Automata Approach to Probabilistic Verification].===		===Michael Huth, Nir Piterman, Daniel Wagner. [http://wiki.ercim.eu/wg/MLQA/images/1/14/Submission_1.pdf p-Automata Approach to Probabilistic Verification].===

	The poster introduces an automata based approach to the		The poster introduces an automata based approach to the

Nataliya at 13:06, 16 July 2010

2010-07-16T13:06:44Z

← Older revision		Revision as of 13:06, 16 July 2010
Line 8:		Line 8:
	There were 11 poster submissions to the MLQA poster session. Click on a poster title in order to access the correspondent poster submission in the pdf format.		There were 11 poster submissions to the MLQA poster session. Click on a poster title in order to access the correspondent poster submission in the pdf format.

	===Michael Huth, Nir Piterman, Daniel Wagner. [p-Automata Approach to Probabilistic Verification].===		===Michael Huth, Nir Piterman, Daniel Wagner. [http://wiki.ercim.eu/wg/MLQA/index.php/Image:Submission_1.pdf p-Automata Approach to Probabilistic Verification].===

	The poster introduces an automata based approach to the		The poster introduces an automata based approach to the

Nataliya at 13:05, 16 July 2010

2010-07-16T13:05:09Z

← Older revision		Revision as of 13:05, 16 July 2010
Line 120:		Line 120:
	through the use of a networking example. It will also contain graphs describing		through the use of a networking example. It will also contain graphs describing
	the evolution of the example over time based on stochastic simulation.		the evolution of the example over time based on stochastic simulation.
	===

		⚫	=== David Cachera, Thomas Jensen, Arnaud Jobin, and Pascal Sotin. A Linear Operator Framework for Analysing Resource Usage. ===
	=== Submission 8 ===
	Corresponding Author: Arnaud Jobin <arnaud.jobin@irisa.fr>
	Title: A Linear Operator Framework for Analysing Resource Usage
⚫	~~Authors:~~ David Cachera, Thomas Jensen, Arnaud Jobin, and Pascal Sotin

	We present a semantics-based framework for analysing the quantitative		We present a semantics-based framework for analysing the quantitative
Line 143:		Line 139:
	energy consumption for a language with complex array operations and		energy consumption for a language with complex array operations and
	explicit energy modes management.		explicit energy modes management.
	===

		⚫	=== Christoffer Sloth and Rafael Wisniewski. Verification of Continuous Dynamical Systems by Timed Automata. ===
	=== Submission 9 ===
	Corresponding Author: Christoffer Sloth <csloth@cs.aau.dk>
⚫	~~Title:~~ Verification of Continuous Dynamical Systems by Timed Automata
	Authors: Christoffer Sloth and Rafael Wisniewski

	The poster outlines a method for abstracting continuous dynamical systems by finite		The poster outlines a method for abstracting continuous dynamical systems by finite
Line 171:		Line 163:
	The proposed abstraction is applied to an example, which illustrates how sound and		The proposed abstraction is applied to an example, which illustrates how sound and
	complete abstractions are generated.		complete abstractions are generated.
	===

		⚫	=== Lei Song, Flemming Nielson, and Bo Friis Nielson. A Broadcast Based Stochastic Calculus. ===
	=== Submission 10 ===
	Corresponding Author: Lei Song <leis@itu.dk>
	Title: A Broadcast Based Stochastic Calculus
⚫	~~Authors:~~ Lei Song, Flemming Nielson, and Bo Friis Nielson

	In our current work we give a stochastic calculus based on broadcast communication. Only		In our current work we give a stochastic calculus based on broadcast communication. Only
Line 185:		Line 173:
	several examples from performance analysis setting such as batch Markovian arrival		several examples from performance analysis setting such as batch Markovian arrival
	process (BMAP), marked markovian arrival process (MMAP) and closed queueing networks.		process (BMAP), marked markovian arrival process (MMAP) and closed queueing networks.
	===

		⚫	=== Massimo Callisto De Donato, Flavio Corradini, Maria Rita Di Berardini, Emanuela Merelli, and Luca Tesei. Tailoring the Shape Calculus for Quantitative Analysis. ===
	=== Submission 11 ===
	Corresponding Author: Massimo Callisto <massimo.callisto@unicam.it>
	Title: Tailoring the Shape Calculus for Quantitative Analysis
⚫	~~Authors:~~ Massimo Callisto De Donato, Flavio Corradini, Maria Rita Di Berardini, Emanuela Merelli, and Luca Tesei

	The Shape Calculus, a bio-inspired language, is a non-deterministic calculus in which processes		The Shape Calculus, a bio-inspired language, is a non-deterministic calculus in which processes
Line 209:		Line 193:
	the calculus and the BioShape tool to work in synergy towards the gaining of quantitative information		the calculus and the BioShape tool to work in synergy towards the gaining of quantitative information
	about simulated environments.		about simulated environments.
	===

Nataliya at 13:02, 16 July 2010

2010-07-16T13:02:53Z

@@ Line 22: / Line 22: @@
 Proceedings of QEST 2010.
 Stochastic process algebras are compositional modelling languages
@@ Line 45: / Line 42: @@
 of IMC using pathway analysis (a type of static analysis), and abstraction
 of PEPA using compositional aggregation of states.
 We present an example of application of SCOWS to a real-life scenario
@@ Line 69: / Line 62: @@
 (the rate at which a clerk processes the submitted loan request) on
 the overall performance of the service.
 In the future tiny devices with microcontrollers and sensors will be in charge
@@ Line 95: / Line 84: @@
 and low resource communication. We model the system as a continuous-time
 Markov chain, and analyze it by posing a number of questions shedding light
-on its behaviour. The properties we are interested in are expressed in continuous
+on its behaviour. The properties we are interested in are expressed in continuous stochastic logic, and probabilistic model checker Prism is used in the analysis.
 Dynamic system adaptation is modeled in Paradigm as coordination of
@@ Line 115: / Line 99: @@
 ration, serves as a stepping stone for quantitative analysis of the
 system during adaptation.
 The link between model checking and static analysis has been of great interest
@@ Line 128: / Line 108: @@
 is static analysis of modal logics and that model checking can be carried by the
 static analysis engine; namely ALFP suite. We use Flow Logic, which is a
 The process algebra HYPE was developed to model hybrid systems which are

Nataliya at 12:53, 16 July 2010

2010-07-16T12:53:32Z

← Older revision		Revision as of 12:53, 16 July 2010
Line 21:		Line 21:
	Discrete-Time Probabilistic Verification" to appear in		Discrete-Time Probabilistic Verification" to appear in
	Proceedings of QEST 2010.		Proceedings of QEST 2010.
	===

	=== Submission 2 ===		=== Submission 2 ===

Nataliya at 12:53, 16 July 2010

2010-07-16T12:53:11Z

← Older revision		Revision as of 12:53, 16 July 2010
Line 8:		Line 8:
	There were 11 poster submissions to the MLQA poster session. Click on a poster title in order to access the correspondent poster submission in the pdf format.		There were 11 poster submissions to the MLQA poster session. Click on a poster title in order to access the correspondent poster submission in the pdf format.

		⚫	===Michael Huth, Nir Piterman, Daniel Wagner. [p-Automata Approach to Probabilistic Verification].===
	MLQA 2010 - Poster Abstracts

	=== Submission 1 ===
	Corresponding Author: Daniel Wagner <d.wagner06@imperial.ac.uk>
⚫	~~Title:~~ p-Automata Approach to Probabilistic Verification
	Authors: Michael Huth, Nir Piterman, Daniel Wagner

	The poster introduces an automata based approach to the		The poster introduces an automata based approach to the