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 712, 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.

Vadim Alimguzhin, Federico Mari, Igor Melatti, Ivano Salvo, and Enrico Tronci. On Model Based Synthesis of Embedded Control Software. Vol. abs/1207.4474. CoRR, Technical Report, 2012.
Abstract: Many Embedded Systems are indeed Software Based Control Systems (SBCSs), 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 control software. Given the formal model of a plant as a Discrete Time Linear Hybrid System and the implementation specifications (that is, number of bits in the AnalogtoDigital (AD) conversion) correctbyconstruction control software can be automatically generated from System Level Formal Specifications of the closed loop system (that is, safety and liveness requirements), by computing a suitable finite abstraction of the plant.
With respect to given implementation specifications, the automatically generated code implements a time optimal control strategy (in terms of setup time), has a Worst Case Execution Time linear in the number of AD bits $b$, but unfortunately, its size grows exponentially with respect to $b$. In many embedded systems, there are severe restrictions on the computational resources (such as memory or computational power) available to microcontroller devices.
This paper addresses model based synthesis of control software by trading system level nonfunctional requirements (such us optimal setup time, ripple) with software nonfunctional requirements (its footprint). Our experimental results show the effectiveness of our approach: for the inverted pendulum benchmark, by using a quantization schema with 12 bits, the size of the small controller is less than 6% of the size of the time optimal one.

T. Mancini, F. Mari, A. Massini, I. Melatti, I. Salvo, and E. Tronci. "On minimising the maximum expected verification time." Information Processing Letters (2017). DOI: 10.1016/j.ipl.2017.02.001.

Enrico Tronci. "On Computing Optimal Controllers for Finite State Systems." In CDC '97: Proceedings of the 36th IEEE International Conference on Decision and Control. Washington, DC, USA: IEEE Computer Society, 1997.

T. Mancini, F. Mari, A. Massini, I. Melatti, and E. Tronci. "On Checking Equivalence of Simulation Scripts." Journal of Logical and Algebraic Methods in Programming (2021): 100640. ISSN: 23522208. DOI: 10.1016/j.jlamp.2021.100640.
Abstract: To support Model Based Design of CyberPhysical Systems (CPSs) many simulation based approaches to System Level Formal Verification (SLFV) have been devised. Basically, these are Bounded Model Checking approaches (since simulation horizon is of course bounded) relying on simulators to compute the system dynamics and thereby verify the given system properties. The main obstacle to simulation based SLFV is the large number of simulation scenarios to be considered and thus the huge amount of simulation time needed to complete the verification task. To save on computation time, simulation based SLFV approaches exploit the capability of simulators to save and restore simulation states. Essentially, such a time saving is obtained by optimising the simulation script defining the simulation activity needed to carry out the verification task. Although such approaches aim to (bounded) formal verification, as a matter of fact, the proof of correctness of the methods to optimise simulation scripts basically relies on an intuitive semantics for simulation scripting languages. This hampers the possibility of formally showing that the optimisations introduced to speed up the simulation activity do not actually omit checking of relevant behaviours for the system under verification. The aim of this paper is to fill the above gap by presenting an operational semantics for simulation scripting languages and by proving soundness and completeness properties for it. This, in turn, enables formal proofs of equivalence between unoptimised and optimised simulation scripts.
Keywords: Formal verification, Simulation based formal verification, Formal Verification of cyberphysical systems, Systemlevel formal verification

T. Mancini. "Now or Never: Negotiating Efficiently with Unknown or Untrusted Counterparts." Fundamenta Informaticae 149, no. 12 (2016): 61–100. DOI: 10.3233/FI20161443.

T. Mancini. "Now or Never: negotiating efficiently with unknown counterparts." In proceedings of the 22nd RCRA International Workshop. Ferrara, Italy. CEUR, 2015 (Colocated with the 14th Conference of the Italian Association for Artificial Intelligence (AI*IA 2015)). (2015).

L. Tortora, G. Meynen, J. Bijlsma, E. Tronci, and S. Ferracuti. "Neuroprediction and A.I. in Forensic Psychiatry and Criminal Justice: A Neurolaw Perspective." Frontiers in Psychology 11 (2020): 220. ISSN: 16641078. DOI: 10.3389/fpsyg.2020.00220.
Abstract: Advances in the use of neuroimaging in combination with A.I., and specifically the use of machine learning techniques, have led to the development of brainreading technologies which, in the nearby future, could have many applications, such as lie detection, neuromarketing or braincomputer interfaces. Some of these could, in principle, also be used in forensic psychiatry. The application of these methods in forensic psychiatry could, for instance, be helpful to increase the accuracy of risk assessment and to identify possible interventions. This technique could be referred to as Ã‚â€˜A.I. neuroprediction,Ã‚â€™ and involves identifying potential neurocognitive markers for the prediction of recidivism. However, the future implications of this technique and the role of neuroscience and A.I. in violence risk assessment remain to be established. In this paper, we review and analyze the literature concerning the use of brainreading A.I. for neuroprediction of violence and rearrest to identify possibilities and challenges in the future use of these techniques in the fields of forensic psychiatry and criminal justice, considering legal implications and ethical issues. The analysis suggests that additional research is required on A.I. neuroprediction techniques, and there is still a great need to understand how they can be implemented in risk assessment in the field of forensic psychiatry. Besides the alluring potential of A.I. neuroprediction, we argue that its use in criminal justice and forensic psychiatry should be subjected to thorough harms/benefits analyses not only when these technologies will be fully available, but also while they are being researched and developed.

M. P. Hengartner, T. H. C. Kruger, K. Geraedts, E. Tronci, T. Mancini, F. Ille, M. Egli, S. RÃ¶blitz, R. Ehrig, L. Saleh et al. "Negative affect is unrelated to fluctuations in hormone levels across the menstrual cycle: Evidence from a multisite observational study across two successive cycles." Journal of Psychosomatic Research 99 (2017): 21–27. DOI: 10.1016/j.jpsychores.2017.05.018.

A. Pappagallo, A. Massini, and E. Tronci. "Monte Carlo Based Statistical Model Checking of CyberPhysical Systems: A Review." Information 11, no. 558 (2020). DOI: 10.3390/info11120588.
