Vadim Alimguzhin, Federico Mari, Igor Melatti, Ivano Salvo, and Enrico Tronci. A Map-Reduce Parallel Approach to Automatic Synthesis of Control Software. Vol. abs/1210.2276. CoRR, Technical Report, 2012.
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.
|
Vadim Alimguzhin, Federico Mari, Igor Melatti, Ivano Salvo, and Enrico Tronci. Automatic Control Software Synthesis for Quantized Discrete Time Hybrid Systems. Vol. abs/1207.4098. CoRR, Technical Report, 2012.
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.
|
Antonio Bucciarelli, Adolfo Piperno, and Ivano Salvo. "Intersection types and λ-definability." Mathematical Structures in Computer Science 13, no. 1 (2003): 15–53. Cambridge University Press. ISSN: 0960-1295. DOI: 10.1017/S0960129502003833.
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.
|
|
Vadim Alimguzhin, Federico Mari, Igor Melatti, Ivano Salvo, and Enrico Tronci. "On Model Based Synthesis of Embedded Control Software." In 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, edited by Ahmed Jerraya and Luca P. Carloni and Florence Maraninchi and John Regehr, 227–236. ACM, 2012. Notes: Techreport version can be found at arxiv.org. DOI: 10.1145/2380356.2380398.
|
|
Federico Mari, Igor Melatti, Ivano Salvo, and Enrico Tronci. "Model Based Synthesis of Control Software from System Level Formal Specifications." ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY 23, no. 1 (2014): Article 6. ACM. ISSN: 1049-331X. DOI: 10.1145/2559934.
|
Benedetto Intrigila, Ivano Salvo, and Stefano Sorgi. "A characterization of weakly Church-Rosser abstract reduction systems that are not Church-Rosser." Information and Computation 171, no. 2 (2001): 137–155. Academic Press, Inc.. ISSN: 0890-5401. DOI: 10.1006/inco.2001.2945.
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.
|
|
Verzino Giovanni, Federico Cavaliere, Federico Mari, Igor Melatti, Giovanni Minei, Ivano Salvo, Yuri Yushtein, and Enrico Tronci. "Model checking driven simulation of sat procedures." In Proceedings of 12th International Conference on Space Operations (SpaceOps 2012)., 2012. DOI: 10.2514/6.2012-1275611.
|
|
T. Mancini, F. Mari, A. Massini, I. Melatti, I. Salvo, S. Sinisi, E. Tronci, R. Ehrig, S. Röblitz, and B. Leeners. "Computing Personalised Treatments through In Silico Clinical Trials. A Case Study on Downregulation in Assisted Reproduction." In 25th RCRA International Workshop on “Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion” (RCRA 2018)., 2018. DOI: 10.29007/g864.
|
|
T. Mancini, F. Mari, I. Melatti, I. Salvo, E. Tronci, J. Gruber, B. Hayes, M. Prodanovic, and L. Elmegaard. "Parallel Statistical Model Checking for Safety Verification in Smart Grids." In 2018 IEEE International Conference on Communications, Control, and Computing Technologies for Smart Grids (SmartGridComm), 1–6., 2018. DOI: 10.1109/SmartGridComm.2018.8587416.
|
|
R. Ehrig, T. Dierkes, S. Schaefer, S. Roeblitz, E. Tronci, T. Mancini, I. Salvo, V. Alimguzhin, F. Mari, I. Melatti et al. "An integrative approach for model driven computation of treatments in reproductive medicine." In Proceedings of the 15th International Symposium on Mathematical and Computational Biology (BIOMAT 2015), Rorkee, India., 2015. DOI: 10.1142/9789813141919_0005.
|
