| |
Records |
Links |
|
Author |
Alimguzhin, Vadim; Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico |
|
| |
Title |
A Map-Reduce Parallel Approach to Automatic Synthesis of Control Software |
Type |
Report |
| |
Year |
2012 |
Publication |
|
Abbreviated Journal |
|
|
| |
Volume |
abs/1210.2276 |
Issue |
|
Pages |
|
|
| |
Keywords |
|
|
| |
Abstract |
Many Control Systems are indeed Software Based Control Systems, i.e. control systems whose controller consists of control software running on a microcontroller device. This motivates investigation on Formal Model Based Design approaches for automatic synthesis of control software.
Available algorithms and tools (e.g., QKS) may require weeks or even months of computation to synthesize control software for large-size systems. This motivates search for parallel algorithms for control software synthesis.
In this paper, we present a map-reduce style parallel algorithm for control software synthesis when the controlled system (plant) is modeled as discrete time linear hybrid system. Furthermore we present an MPI-based implementation PQKS of our algorithm. To the best of our knowledge, this is the first parallel approach for control software synthesis.
We experimentally show effectiveness of PQKS on two classical control synthesis problems: the inverted pendulum and the multi-input buck DC/DC converter. Experiments show that PQKS efficiency is above 65%. As an example, PQKS requires about 16 hours to complete the synthesis of control software for the pendulum on a cluster with 60 processors, instead of the 25 days needed by the sequential algorithm in QKS. |
|
| |
Address |
|
|
| |
Corporate Author |
|
Thesis |
|
|
| |
Publisher  |
CoRR, Technical Report |
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 @ |
Serial |
101 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Alimguzhin, Vadim; Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico |
|
| |
Title |
Automatic Control Software Synthesis for Quantized Discrete Time Hybrid Systems |
Type |
Report |
| |
Year |
2012 |
Publication |
|
Abbreviated Journal |
|
|
| |
Volume |
abs/1207.4098 |
Issue |
|
Pages |
|
|
| |
Keywords |
|
|
| |
Abstract |
Many Embedded Systems are indeed Software Based Control Systems, that is control systems whose controller consists of control software running on a microcontroller device. This motivates investigation on Formal Model Based Design approaches for automatic synthesis of embedded systems control software. This paper addresses control software synthesis for discrete time nonlinear systems. We present a methodology to overapproximate the dynamics of a discrete time nonlinear hybrid system H by means of a discrete time linear hybrid system L(H), in such a way that controllers for L(H) are guaranteed to be controllers for H. We present experimental results on the inverted pendulum, a challenging and meaningful benchmark in nonlinear Hybrid Systems control. |
|
| |
Address |
|
|
| |
Corporate Author |
|
Thesis |
|
|
| |
Publisher |
CoRR, Technical Report |
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 @ |
Serial |
103 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Bucciarelli, Antonio; Piperno, Adolfo; Salvo, Ivano |
|
| |
Title |
Intersection types and λ-definability |
Type |
Journal Article |
| |
Year |
2003 |
Publication |
Mathematical Structures in Computer Science |
Abbreviated Journal |
|
|
| |
Volume |
13 |
Issue |
1 |
Pages |
15-53 |
|
| |
Keywords |
|
|
| |
Abstract |
This paper presents a novel method for comparing computational properties of λ-terms that are typeable with intersection types, with respect to terms that are typeable with Curry types. We introduce a translation from intersection typing derivations to Curry typeable terms that is preserved by β-reduction: this allows the simulation of a computation starting from a term typeable in the intersection discipline by means of a computation starting from a simply typeable term. Our approach proves strong normalisation for the intersection system naturally by means of purely syntactical techniques. The paper extends the results presented in Bucciarelli et al. (1999) to the whole intersection type system of Barendregt, Coppo and Dezani, thus providing a complete proof of the conjecture, proposed in Leivant (1990), that all functions uniformly definable using intersection types are already definable using Curry types. |
|
| |
Address |
|
|
| |
Corporate Author |
|
Thesis |
|
|
| |
Publisher |
Cambridge University Press |
Place of Publication |
New York, NY, USA |
Editor |
|
|
| |
Language |
|
Summary Language |
|
Original Title |
|
|
| |
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
|
| |
Series Volume |
|
Series Issue |
|
Edition |
|
|
| |
ISSN |
0960-1295 |
ISBN |
|
Medium |
|
|
| |
Area |
|
Expedition |
|
Conference |
|
|
| |
Notes |
|
Approved |
yes |
|
| |
Call Number |
Sapienza @ mari @ Bucciarelli-Piperno-Salvo:MSCS-03 |
Serial |
69 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Alimguzhin, Vadim; Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico |
|
| |
Title |
On Model Based Synthesis of Embedded Control Software |
Type |
Conference Article |
| |
Year |
2012 |
Publication |
Proceedings of the 12th International Conference on Embedded Software, EMSOFT 2012, part of the Eighth Embedded Systems Week, ESWeek 2012, Tampere, Finland, October 7-12, 2012 |
Abbreviated Journal |
|
|
| |
Volume |
|
Issue |
|
Pages |
227-236 |
|
| |
Keywords |
|
|
| |
Abstract |
|
|
| |
Address |
|
|
| |
Corporate Author |
|
Thesis |
|
|
| |
Publisher |
ACM |
Place of Publication |
|
Editor |
Ahmed Jerraya and Luca P. Carloni and Florence Maraninchi and John Regehr |
|
| |
Language |
|
Summary Language |
|
Original Title |
|
|
| |
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
|
| |
Series Volume |
|
Series Issue |
|
Edition |
|
|
| |
ISSN |
|
ISBN |
978-1-4503-1425-1 |
Medium |
|
|
| |
Area |
|
Expedition |
|
Conference |
|
|
| |
Notes |
Techreport version can be found at arxiv.org |
Approved |
yes |
|
| |
Call Number |
Sapienza @ mari @ emsoft12 |
Serial |
97 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico |
|
| |
Title |
Model Based Synthesis of Control Software from System Level Formal Specifications |
Type |
Journal Article |
| |
Year |
2014 |
Publication |
ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY |
Abbreviated Journal |
ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY |
|
| |
Volume |
23 |
Issue |
1 |
Pages |
Article 6 |
|
| |
Keywords |
|
|
| |
Abstract |
|
|
| |
Address |
|
|
| |
Corporate Author |
|
Thesis |
|
|
| |
Publisher |
ACM |
Place of Publication |
|
Editor |
|
|
| |
Language |
|
Summary Language |
|
Original Title |
|
|
| |
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
|
| |
Series Volume |
|
Series Issue |
|
Edition |
|
|
| |
ISSN |
1049-331X |
ISBN |
|
Medium |
|
|
| |
Area |
|
Expedition |
|
Conference |
|
|
| |
Notes |
|
Approved |
no |
|
| |
Call Number |
Sapienza @ melatti @ |
Serial |
110 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Intrigila, Benedetto; Salvo, Ivano; Sorgi, Stefano |
|
| |
Title |
A characterization of weakly Church-Rosser abstract reduction systems that are not Church-Rosser |
Type |
Journal Article |
| |
Year |
2001 |
Publication |
Information and Computation |
Abbreviated Journal |
|
|
| |
Volume |
171 |
Issue |
2 |
Pages |
137-155 |
|
| |
Keywords |
|
|
| |
Abstract |
Basic properties of rewriting systems can be stated in the framework of abstract reduction systems (ARS). Properties like confluence (or Church-Rosser, CR) and weak confluence (or weak Church-Rosser, WCR) and their relationships can be studied in this setting: as a matter of fact, well-known counterexamples to the implication WCR CR have been formulated as ARS. In this paper, starting from the observation that such counterexamples are structurally similar, we set out a graph-theoretic characterization of WCR ARS that is not CR in terms of a suitable class of reduction graphs, such that in every WCR not CR ARS, we can embed at least one element of this class. Moreover, we give a tighter characterization for a restricted class of ARS enjoying a suitable regularity condition. Finally, as a consequence of our approach, we prove some interesting results about ARS using the mathematical tools developed. In particular, we prove an extension of the Newman’s lemma and we find out conditions that, once assumed together with WCR property, ensure the unique normal form property. The Appendix treats two interesting examples, both generated by graph-rewriting rules, with specific combinatorial properties. |
|
| |
Address |
|
|
| |
Corporate Author |
|
Thesis |
|
|
| |
Publisher |
Academic Press, Inc. |
Place of Publication |
Duluth, MN, USA |
Editor |
|
|
| |
Language |
|
Summary Language |
|
Original Title |
|
|
| |
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
|
| |
Series Volume |
|
Series Issue |
|
Edition |
|
|
| |
ISSN |
0890-5401 |
ISBN |
|
Medium |
|
|
| |
Area |
|
Expedition |
|
Conference |
|
|
| |
Notes |
|
Approved |
yes |
|
| |
Call Number |
Sapienza @ mari @ Intrigila-Salvo-Sorgi:01 |
Serial |
68 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Verzino Giovanni ; Cavaliere, Federico; Mari, Federico; Melatti, Igor; Minei, Giovanni; Salvo, Ivano; Yushtein, Yuri; Tronci, Enrico |
|
| |
Title |
Model checking driven simulation of sat procedures |
Type |
Conference Article |
| |
Year |
2012 |
Publication |
Proceedings of 12th International Conference on Space Operations (SpaceOps 2012) |
Abbreviated Journal |
International Conference on Space Operations |
|
| |
Volume |
|
Issue |
|
Pages |
|
|
| |
Keywords |
|
|
| |
Abstract |
|
|
| |
Address |
|
|
| |
Corporate Author |
|
Thesis |
|
|
| |
Publisher |
|
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 |
117 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Mancini, T.; Mari, F.; Massini, A.; Melatti, I.; Salvo, I.; Sinisi, S.; Tronci, E.; Ehrig, R.; Röblitz, S.; Leeners, B. |
|
| |
Title |
Computing Personalised Treatments through In Silico Clinical Trials. A Case Study on Downregulation in Assisted Reproduction |
Type |
Conference Article |
| |
Year |
2018 |
Publication |
25th RCRA International Workshop on “Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion” (RCRA 2018) |
Abbreviated Journal |
|
|
| |
Volume |
|
Issue |
|
Pages |
|
|
| |
Keywords |
|
|
| |
Abstract |
|
|
| |
Address |
|
|
| |
Corporate Author |
|
Thesis |
|
|
| |
Publisher |
|
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 @ |
Serial |
175 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Mancini, T.; Mari, F.; Melatti, I.; Salvo, I.; Tronci, E.; Gruber, J.; Hayes, B.; Prodanovic, M.; Elmegaard, L. |
|
| |
Title |
Parallel Statistical Model Checking for Safety Verification in Smart Grids |
Type |
Conference Article |
| |
Year |
2018 |
Publication |
2018 IEEE International Conference on Communications, Control, and Computing Technologies for Smart Grids (SmartGridComm) |
Abbreviated Journal |
|
|
| |
Volume |
|
Issue |
|
Pages |
1-6 |
|
| |
Keywords |
|
|
| |
Abstract |
|
|
| |
Address |
|
|
| |
Corporate Author |
|
Thesis |
|
|
| |
Publisher |
|
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 @ mancini-etal:2018:smartgridcomm |
Serial |
170 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Ehrig, R.; Dierkes, T.; Schaefer, S.; Roeblitz, S.; Tronci, E.; Mancini, T.; Salvo, I.; Alimguzhin, V.; Mari, F.; Melatti, I.; Massini, A.; Leeners, B.; Krueger, T.H.C.; Egli, M.; Ille, F. |
|
| |
Title |
An integrative approach for model driven computation of treatments in reproductive medicine |
Type |
Conference Article |
| |
Year |
2015 |
Publication |
Proceedings of the 15th International Symposium on Mathematical and Computational Biology (BIOMAT 2015), Rorkee, India |
Abbreviated Journal |
|
|
| |
Volume |
|
Issue |
|
Pages |
|
|
| |
Keywords |
|
|
| |
Abstract |
|
|
| |
Address |
|
|
| |
Corporate Author |
|
Thesis |
|
|
| |
Publisher |
|
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 @ preissler @ Ehrig_etal2015 |
Serial |
144 |
|
| Permanent link to this record |
