MCLab Group List of Papers -- Query Results

	MCLab Group List of Papers Home \| Show All \| Simple Search \| Advanced Search	Login Quick Search: Field: contains: ...
	121–130 of 143 records found matching your query (RSS \| history):

Search & Display Options

Select All Deselect All

[1–10] << 11 12 13 14 15 >>

List View

Citations

Details

	Records
	Author	Della Penna, Giuseppe; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico; Venturini Zilli, Marisa
	Title	Finite Horizon Analysis of Stochastic Systems with the Mur$\varphi$ Verifier			Type	Conference Article
	Year	2003	Publication	Theoretical Computer Science, 8th Italian Conference, ICTCS 2003, Bertinoro, Italy, October 13-15, 2003, Proceedings	Abbreviated Journal
	Volume		Issue		Pages	58-71
	Keywords
	Abstract	Many reactive systems are actually Stochastic Processes. Automatic analysis of such systems is usually very difficult thus typically one simplifies the analysis task by using simulation or by working on a simplified model (e.g. a Markov Chain). We present a Finite Horizon Probabilistic Model Checking approach which essentially can handle the same class of stochastic processes of a typical simulator. This yields easy modeling of the system to be analyzed together with formal verification capabilities. Our approach is based on a suitable disk based extension of the Mur$\varphi$ verifier. Moreover we present experimental results showing effectiveness of our approach.
	Address
	Corporate Author				Thesis
	Publisher	Springer	Place of Publication		Editor	Blundo, C.; Laneve, C.
	Language		Summary Language		Original Title
	Series Editor		Series Title	Lecture Notes in Computer Science	Abbreviated Series Title
	Series Volume	2841	Series Issue		Edition
	ISSN	3-540-20216-1	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ DIMTZ03c			Serial	90
Permanent link to this record



	Author	Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico; Alvisi, Lorenzo; Clement, Allen; Li, Harry
	Title	Model Checking Nash Equilibria in MAD Distributed Systems			Type	Conference Article
	Year	2008	Publication	FMCAD '08: Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design	Abbreviated Journal
	Volume		Issue		Pages	1-8
	Keywords	Model Checking, MAD Distributed System, Nash Equilibrium
	Abstract	We present a symbolic model checking algorithm for verification of Nash equilibria in finite state mechanisms modeling Multiple Administrative Domains (MAD) distributed systems. Given a finite state mechanism, a proposed protocol for each agent and an indifference threshold for rewards, our model checker returns PASS if the proposed protocol is a Nash equilibrium (up to the given indifference threshold) for the given mechanism, FAIL otherwise. We implemented our model checking algorithm inside the NuSMV model checker and present experimental results showing its effectiveness for moderate size mechanisms. For example, we can handle mechanisms which corresponding normal form games would have more than $10^20$ entries. To the best of our knowledge, no model checking algorithm for verification of mechanism Nash equilibria has been previously published.
	Address
	Corporate Author				Thesis
	Publisher	IEEE Press	Place of Publication	Piscataway, NJ, USA	Editor	Cimatti, A.; Jones, R.
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN	978-1-4244-2735-2	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ MarMelSalTroAlvCle08			Serial	93
Permanent link to this record



	Author	Della Penna, Giuseppe; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico
	Title	Exploiting Hub States in Automatic Verification			Type	Conference Article
	Year	2005	Publication	Automated Technology for Verification and Analysis: Third International Symposium, ATVA 2005, Taipei, Taiwan, October 4-7, 2005, Proceedings	Abbreviated Journal
	Volume		Issue		Pages	54-68
	Keywords
	Abstract	In this paper we present a new algorithm to counteract state explosion when using Explicit State Space Exploration to verify protocol-like systems. We sketch the implementation of our algorithm within the Caching Mur$\varphi$ verifier and give experimental results showing its effectiveness. We show experimentally that, when memory is a scarce resource, our algorithm improves on the time performances of Caching Mur$\varphi$ verification algorithm, saving between 16% and 68% (45% on average) in computation time.
	Address
	Corporate Author				Thesis
	Publisher	Springer	Place of Publication		Editor	D.A. Peled; Y.-K. Tsay
	Language		Summary Language		Original Title
	Series Editor		Series Title	Lecture Notes in Computer Science	Abbreviated Series Title
	Series Volume	3707	Series Issue		Edition
	ISSN	3-540-29209-8	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ Dimt04			Serial	83
Permanent link to this record



	Author	Pugliese, Rosario; Tronci, Enrico
	Title	Automatic Verification of a Hydroelectric Power Plant			Type	Conference Article
	Year	1996	Publication	Third International Symposium of Formal Methods Europe (FME), Co-Sponsored by IFIP WG 14.3	Abbreviated Journal
	Volume		Issue		Pages	425-444
	Keywords
	Abstract	We analyze the specification of a hydroelectric power plant by ENEL (the Italian Electric Company). Our goal is to show that for the specification of the plant (its control system in particular) some given properties hold. We were provided with an informal specification of the plant. From such informal specification we wrote a formal specification using the CCS/Meije process algebra formalism. We defined properties using μ-calculus. Automatic verification was carried out using model checking. This was done by translating our process algebra definitions (the model) and μ-calculus formulas into BDDs. In this paper we present the informal specification of the plant, its formal specification, some of the properties we verified and experimental results.
	Address
	Corporate Author				Thesis
	Publisher	Springer	Place of Publication	Oxford, UK	Editor	Gaudel, M.-C.; Woodcock, J.
	Language		Summary Language		Original Title
	Series Editor		Series Title	Lecture Notes in Computer Science	Abbreviated Series Title
	Series Volume	1051	Series Issue		Edition
	ISSN	3-540-60973-3	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ fme96			Serial	53
Permanent link to this record



	Author
	Title	Charme			Type	Conference Article
	Year	2003	Publication	Lecture Notes in Computer Science	Abbreviated Journal
	Volume	2860	Issue		Pages
	Keywords
	Abstract
	Address
	Corporate Author				Thesis
	Publisher	Springer	Place of Publication		Editor	Geist, D.; Tronci, E.
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN	3-540-20363-X	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ editor-charme03			Serial	37
Permanent link to this record



	Author	Della Penna, Giuseppe; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico; Venturini Zilli, Marisa
	Title	Finite Horizon Analysis of Markov Chains with the Mur$\varphi$ Verifier			Type	Conference Article
	Year	2003	Publication	Correct Hardware Design and Verification Methods, 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L'Aquila, Italy, October 21-24, 2003, Proceedings	Abbreviated Journal
	Volume		Issue		Pages	394-409
	Keywords
	Abstract	In this paper we present an explicit disk based verification algorithm for Probabilistic Systems defining discrete time/finite state Markov Chains. Given a Markov Chain and an integer k (horizon), our algorithm checks whether the probability of reaching an error state in at most k steps is below a given threshold. We present an implementation of our algorithm within a suitable extension of the Mur$\varphi$ verifier. We call the resulting probabilistic model checker FHP-Mur$\varphi$ (Finite Horizon Probabilistic Mur$\varphi$). We present experimental results comparing FHP-Mur$\varphi$ with (a finite horizon subset of) PRISM, a state-of-the-art symbolic model checker for Markov Chains. Our experimental results show that FHP-Mur$\varphi$ can handle systems that are out of reach for PRISM, namely those involving arithmetic operations on the state variables (e.g. hybrid systems).
	Address
	Corporate Author				Thesis
	Publisher	Springer	Place of Publication		Editor	Geist, D.; Tronci, E.
	Language		Summary Language		Original Title
	Series Editor		Series Title	Lecture Notes in Computer Science	Abbreviated Series Title
	Series Volume	2860	Series Issue		Edition
	ISSN	3-540-20363-X	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ Dimtz03			Serial	84
Permanent link to this record



	Author	Della Penna, Giuseppe; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico; Venturini Zilli, Marisa
	Title	Integrating RAM and Disk Based Verification within the Mur$\varphi$ Verifier			Type	Conference Article
	Year	2003	Publication	Correct Hardware Design and Verification Methods, 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L'Aquila, Italy, October 21-24, 2003, Proceedings	Abbreviated Journal
	Volume		Issue		Pages	277-282
	Keywords
	Abstract	We present a verification algorithm that can automatically switch from RAM based verification to disk based verification without discarding the work done during the RAM based verification phase. This avoids having to choose beforehand the proper verification algorithm. Our experimental results show that typically our integrated algorithm is as fast as (sometime faster than) the fastest of the two base (i.e. RAM based and disk based) verification algorithms.
	Address
	Corporate Author				Thesis
	Publisher	Springer	Place of Publication		Editor	Geist, D.; Tronci, E.
	Language		Summary Language		Original Title
	Series Editor		Series Title	Lecture Notes in Computer Science	Abbreviated Series Title
	Series Volume	2860	Series Issue		Edition
	ISSN	3-540-20363-X	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ DIMTZ03a			Serial	85
Permanent link to this record



	Author	Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico; Alvisi, Lorenzo; Clement, Allen; Li, Harry
	Title	Model Checking Coalition Nash Equilibria in MAD Distributed Systems			Type	Conference Article
	Year	2009	Publication	Stabilization, Safety, and Security of Distributed Systems, 11th International Symposium, SSS 2009, Lyon, France, November 3-6, 2009. Proceedings	Abbreviated Journal
	Volume		Issue		Pages	531-546
	Keywords
	Abstract	We present two OBDD based model checking algorithms for the verification of Nash equilibria in finite state mechanisms modeling Multiple Administrative Domains (MAD) distributed systems with possibly colluding agents (coalitions) and with possibly faulty or malicious nodes (Byzantine agents). Given a finite state mechanism, a proposed protocol for each agent and the maximum sizes f for Byzantine agents and q for agents collusions, our model checkers return Pass if the proposed protocol is an ε-f-q-Nash equilibrium, i.e. no coalition of size up to q may have an interest greater than ε in deviating from the proposed protocol when up to f Byzantine agents are present, Fail otherwise. We implemented our model checking algorithms within the NuSMV model checker: the first one explicitly checks equilibria for each coalition, while the second represents symbolically all coalitions. We present experimental results showing their effectiveness for moderate size mechanisms. For example, we can verify coalition Nash equilibria for mechanisms which corresponding normal form games would have more than $5 \times 10^21$ entries. Moreover, we compare the two approaches, and the explicit algorithm turns out to outperform the symbolic one. To the best of our knowledge, no model checking algorithm for verification of Nash equilibria of mechanisms with coalitions has been previously published.
	Address
	Corporate Author				Thesis
	Publisher	Springer	Place of Publication		Editor	Guerraoui, R.; Petit, F.
	Language		Summary Language		Original Title
	Series Editor		Series Title	Lecture Notes in Computer Science	Abbreviated Series Title
	Series Volume	5873	Series Issue		Edition
	ISSN		ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ sss09			Serial	19
Permanent link to this record



	Author	Della Penna, Giuseppe; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico; Venturini Zilli, Marisa
	Title	Bounded Probabilistic Model Checking with the Mur$\varphi$ Verifier			Type	Conference Article
	Year	2004	Publication	Formal Methods in Computer-Aided Design, 5th International Conference, FMCAD 2004, Austin, Texas, USA, November 15-17, 2004, Proceedings	Abbreviated Journal
	Volume		Issue		Pages	214-229
	Keywords
	Abstract	In this paper we present an explicit verification algorithm for Probabilistic Systems defining discrete time/finite state Markov Chains. We restrict ourselves to verification of Bounded PCTL formulas (BPCTL), that is, PCTL formulas in which all Until operators are bounded, possibly with different bounds. This means that we consider only paths (system runs) of bounded length. Given a Markov Chain $\cal M$ and a BPCTL formula Φ, our algorithm checks if Φ is satisfied in $\cal M$. This allows to verify important properties, such as reliability in Discrete Time Hybrid Systems. We present an implementation of our algorithm within a suitable extension of the Mur$\varphi$ verifier. We call FHP-Mur$\varphi$ (Finite Horizon Probabilistic Mur$\varphi$) such extension of the Mur$\varphi$ verifier. We give experimental results comparing FHP-Mur$\varphi$ with (a finite horizon subset of) PRISM, a state-of-the-art symbolic model checker for Markov Chains. Our experimental results show that FHP-Mur$\varphi$ can effectively handle verification of BPCTL formulas for systems that are out of reach for PRISM, namely those involving arithmetic operations on the state variables (e.g. hybrid systems).
	Address
	Corporate Author				Thesis
	Publisher	Springer	Place of Publication		Editor	Hu, A.J.; Martin, A.K.
	Language		Summary Language		Original Title
	Series Editor		Series Title	Lecture Notes in Computer Science	Abbreviated Series Title
	Series Volume	3312	Series Issue		Edition
	ISSN	3-540-23738-0	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ Dimtz04			Serial	87
Permanent link to this record



	Author	Fantechi, Alessandro; Gnesi, Stefania; Mazzanti, Franco; Pugliese, Rosario; Tronci, Enrico
	Title	A Symbolic Model Checker for ACTL			Type	Conference Article
	Year	1998	Publication	International Workshop on Current Trends in Applied Formal Method (FM-Trends)	Abbreviated Journal
	Volume		Issue		Pages	228-242
	Keywords
	Abstract	We present SAM, a symbolic model checker for ACTL, the action-based version of CTL. SAM relies on implicit representations of Labeled Transition Systems (LTSs), the semantic domain for ACTL formulae, and uses symbolic manipulation algorithms. SAM has been realized by translating (networks of) LTSs and, possibly recursive, ACTL formulae into BSP (Boolean Symbolic Programming), a programming language aiming at defining computations on boolean functions, and by using the BSP interpreter to carry out computations (i.e. verifications).
	Address
	Corporate Author				Thesis
	Publisher	Springer	Place of Publication	Boppard, Germany	Editor	Hutter, D.; Stephan, W.; Traverso, P.; Ullmann, M.
	Language		Summary Language		Original Title
	Series Editor		Series Title	Lecture Notes in Computer Science	Abbreviated Series Title
	Series Volume	1641	Series Issue		Edition
	ISSN	3-540-66462-9	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ fm-trends98			Serial	51
Permanent link to this record