MCLab Group List of Papers -- Query Results

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

Search & Display Options

Select All Deselect All

<< 1 2 3 4 5 6 7 8 9 10 >> [11–13]

List View

Citations

Details

	Records
	Author	Della Penna, Giuseppe; Magazzeni, Daniele; Tofani, Alberto; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico
	Title	Automatic Synthesis of Robust Numerical Controllers			Type	Conference Article
	Year	2007	Publication	Icas '07	Abbreviated Journal
	Volume		Issue		Pages	4
	Keywords
	Abstract	A major problem of numerical controllers is their robustness, i.e. the state read from the plant may not be in the controller table, although it may be close to some states in the table. For continuous systems, this problem is typically handled by interpolation techniques. Unfortunately, when the plant contains both continuous and discrete variables, the interpolation approach does not work well. To cope with this kind of systems, we propose a general methodology that exploits explicit model checking in an innovative way to automatically synthesize a (time-) optimal numerical controller from a plant specification and apply an optimized strengthening algorithm only on the most significant states, in order to reach an acceptable robustness degree. We implemented all the algorithms within our CGMurphi tool, an extension of the well-known CMurphi verifier, and tested the effectiveness of our approach by applying it to the well-known truck and trailer obstacles avoidance problem.
	Address
	Corporate Author				Thesis
	Publisher	IEEE Computer Society	Place of Publication		Editor
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN	0-7695-2859-5	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ Dmtimt07			Serial	89
Permanent link to this record



	Author	Mancini, Toni ; Mari, Federico ; Massini, Annalisa; Melatti, Igor; Tronci, Enrico
	Title	System Level Formal Verification via Distributed Multi-Core Hardware in the Loop Simulation			Type	Conference Article
	Year	2014	Publication	Proc. of the 22nd Euromicro International Conference on Parallel, Distributed and Network-Based Processing	Abbreviated Journal	Euromicro International Conference on Parallel, Distributed and Network-Based Processing
	Volume		Issue		Pages
	Keywords
	Abstract
	Address
	Corporate Author				Thesis
	Publisher	IEEE Computer Society	Place of Publication		Editor
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN		ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	no
	Call Number	Sapienza @ melatti @			Serial	118
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; Magazzeni, Daniele; Tofani, Alberto; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico
	Title	Automated Generation of Optimal Controllers through Model Checking Techniques			Type	Conference Article
	Year	2006	Publication	Icinco-Icso	Abbreviated Journal
	Volume		Issue		Pages	26-33
	Keywords
	Abstract	We present a methodology for the synthesis of controllers, which exploits (explicit) model checking techniques. That is, we can cope with the systematic exploration of a very large state space. This methodology can be applied to systems where other approaches fail. In particular, we can consider systems with an highly non-linear dynamics and lacking a uniform mathematical description (model). We can also consider situations where the required control action cannot be specified as a local action, and rather a kind of planning is required. Our methodology individuates first a raw optimal controller, then extends it to obtain a more robust one. A case study is presented which considers the well known truck-trailer obstacle avoidance parking problem, in a parking lot with obstacles on it. The complex non-linear dynamics of the truck-trailer system, within the presence of obstacles, makes the parking problem extremely hard. We show how, by our methodology, we can obtain optimal controllers with different degrees of robustness.
	Address
	Corporate Author				Thesis
	Publisher	INSTICC Press	Place of Publication		Editor	Andrade-Cetto, J.; Ferrier, J.-L.; Pereira, J. M. C. D.; Filipe, J.
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN	972-8865-59-7	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ Dimmtt06			Serial	79
Permanent link to this record



	Author	Driouich, Y.; Parente, M.; Tronci, E.
	Title	Model Checking Cyber-Physical Energy Systems			Type	Conference Article
	Year	2018	Publication	Proceedings of 2017 International Renewable and Sustainable Energy Conference, IRSEC 2017	Abbreviated Journal
	Volume		Issue		Pages
	Keywords
	Abstract
	Address
	Corporate Author				Thesis
	Publisher	Institute of Electrical and Electronics Engineers Inc.	Place of Publication		Editor
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN		ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	no
	Call Number	MCLab @ davi @ Driouich2018			Serial	177
Permanent link to this record



	Author	Mari, Federico; Melatti, Igor; Tronci, Enrico; Finzi, Alberto
	Title	A multi-hop advertising discovery and delivering protocol for multi administrative domain MANET			Type	Journal Article
	Year	2013	Publication	Mobile Information Systems	Abbreviated Journal	Mobile Information Systems
	Volume	3	Issue	9	Pages	261-280
	Keywords
	Abstract
	Address
	Corporate Author				Thesis
	Publisher	IOS Press	Place of Publication		Editor
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN	1574-017x (Print) 1875-905X (Online)	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	no
	Call Number	Sapienza @ melatti @			Serial	109
Permanent link to this record



	Author	Sinisi, S.; Alimguzhin, V.; Mancini, T.; Tronci, E.; Mari, F.; Leeners, B.
	Title	Optimal Personalised Treatment Computation through In Silico Clinical Trials on Patient Digital Twins			Type	Journal Article
	Year	2020	Publication		Abbreviated Journal	Fundamenta Informaticae
	Volume	174	Issue		Pages	283-310
	Keywords	Artificial Intelligence; Virtual Physiological Human; In Silico Clinical Trials; Simulation; Personalised Medicine; In Silico Treatment Optimisation
	Abstract	In Silico Clinical Trials (ISCT), i.e. clinical experimental campaigns carried out by means of computer simulations, hold the promise to decrease time and cost for the safety and efficacy assessment of pharmacological treatments, reduce the need for animal and human testing, and enable precision medicine. In this paper we present methods and an algorithm that, by means of extensive computer simulation-based experimental campaigns (ISCT) guided by intelligent search, optimise a pharmacological treatment for an individual patient (precision medicine ). We show the effectiveness of our approach on a case study involving a real pharmacological treatment, namely the downregulation phase of a complex clinical protocol for assisted reproduction in humans.
	Address
	Corporate Author				Thesis
	Publisher	IOS Press	Place of Publication		Editor
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN	1875-8681	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	no
	Call Number	MCLab @ davi @			Serial	187
Permanent link to this record



	Author	Chen, Q.M.; Finzi, A.; Mancini, T.; Melatti, I.; Tronci, E.
	Title	MILP, Pseudo-Boolean, and OMT Solvers for Optimal Fault-Tolerant Placements of Relay Nodes in Mission Critical Wireless Networks			Type	Journal Article
	Year	2020	Publication		Abbreviated Journal	Fundamenta Informaticae
	Volume	174	Issue		Pages	229-258
	Keywords
	Abstract	In critical infrastructures like airports, much care has to be devoted in protecting radio communication networks from external electromagnetic interference. Protection of such mission-critical radio communication networks is usually tackled by exploiting radiogoniometers: at least three suitably deployed radiogoniometers, and a gateway gathering information from them, permit to monitor and localise sources of electromagnetic emissions that are not supposed to be present in the monitored area. Typically, radiogoniometers are connected to the gateway through relay nodes . As a result, some degree of fault-tolerance for the network of relay nodes is essential in order to offer a reliable monitoring. On the other hand, deployment of relay nodes is typically quite expensive. As a result, we have two conflicting requirements: minimise costs while guaranteeing a given fault-tolerance. In this paper, we address the problem of computing a deployment for relay nodes that minimises the overall cost while at the same time guaranteeing proper working of the network even when some of the relay nodes (up to a given maximum number) become faulty (fault-tolerance ). We show that, by means of a computation-intensive pre-processing on a HPC infrastructure, the above optimisation problem can be encoded as a 0/1 Linear Program, becoming suitable to be approached with standard Artificial Intelligence reasoners like MILP, PB-SAT, and SMT/OMT solvers. Our problem formulation enables us to present experimental results comparing the performance of these three solving technologies on a real case study of a relay node network deployment in areas of the Leonardo da Vinci Airport in Rome, Italy.
	Address
	Corporate Author				Thesis
	Publisher	IOS Press	Place of Publication		Editor
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN	1875-8681	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	no
	Call Number	MCLab @ davi @			Serial	188
Permanent link to this record



	Author	Della Penna, Giuseppe; Magazzeni, Daniele; Tofani, Alberto; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico
	Title	Automated Generation Of Optimal Controllers Through Model Checking Techniques			Type	Book Chapter
	Year	2008	Publication	Informatics in Control Automation and Robotics. Selected Papers from ICINCO 2006	Abbreviated Journal
	Volume		Issue		Pages	107-119
	Keywords
	Abstract
	Address
	Corporate Author				Thesis
	Publisher	Springer	Place of Publication		Editor
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN		ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ Dmtmt08			Serial	26
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