arXiv subjects

Marco Roveri

Publications and source records attributed to Marco Roveri.

25 records · Page 2Linked to original sources

arXiv2022

A Markovian Model for the Spread of the SARS-CoV-2 Virus

We propose a Markovian stochastic approach to model the spread of a SARS-CoV-2-like infection within a closed group of humans. The model takes the form of a Partially Observable Markov Decision Process (POMDP), whose states are given by the number of subjects in different health conditions. The model also exposes the different parameters that have an impact on the spread of the disease and the various decision variables that can be used to control it (e.g, social distancing, number of tests administered to single out infected subjects). The model describes the stochastic phenomena that underlie the spread of the epidemic and captures, in the form of deterministic parameters, some fundamental limitations in the availability of resources (hospital beds and test swabs). The model lends itself to different uses. For a given control policy, it is possible to verify if it satisfies an analytical property on the stochastic evolution of the state (e.g., to compute probability that the hospital beds will reach a fill level, or that a specified percentage of the population will die). If the control policy is not given, it is possible to apply POMDP techniques to identify an optimal control policy that fulfils some specified probabilistic goals. Whilst the paper primarily aims at the model description, we show with numeric examples some of its potential applications.

eess.SY↗

arXiv2022

Computing unsatisfiable cores for LTLf specifications

Linear-time temporal logic on finite traces (LTLf) is rapidly becoming a de-facto standard to produce specifications in many application domains (e.g., planning, business process management, run-time monitoring, reactive synthesis). Several studies approached the respective satisfiability problem. In this paper, we investigate the problem of extracting the unsatisfiable core in LTLf specifications. We provide four algorithms for extracting an unsatisfiable core leveraging the adaptation of state-of-the-art approaches to LTLf satisfiability checking. We implement the different approaches within the respective tools and carry out an experimental evaluation on a set of reference benchmarks, restricting to the unsatisfiable ones. The results show the feasibility, effectiveness, and complementarities of the different algorithms and tools.

cs.LO↗

arXiv2018

Satisfiability Modulo Transcendental Functions via Incremental Linearization

In this paper we present an abstraction-refinement approach to Satisfiability Modulo the theory of transcendental functions, such as exponentiation and trigonometric functions. The transcendental functions are represented as uninterpreted in the abstract space, which is described in terms of the combined theory of linear arithmetic on the rationals with uninterpreted functions, and are incrementally axiomatized by means of upper- and lower-bounding piecewise-linear functions. Suitable numerical techniques are used to ensure that the abstractions of the transcendental functions are sound even in presence of irrationals. Our experimental evaluation on benchmarks from verification and mathematics demonstrates the potential of our approach, showing that it compares favorably with delta-satisfiability /interval propagation and methods based on theorem proving.

cs.LO↗

arXiv2018

Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF

Model checking invariant properties of designs, represented as transition systems, with non-linear real arithmetic (NRA), is an important though very hard problem. On the one hand NRA is a hard-to-solve theory; on the other hand most of the powerful model checking techniques lack support for NRA. In this paper, we present a counterexample-guided abstraction refinement (CEGAR) approach that leverages linearization techniques from differential calculus to enable the use of mature and efficient model checking algorithms for transition systems on linear real arithmetic (LRA) with uninterpreted functions (EUF). The results of an empirical evaluation confirm the validity and potential of this approach.

cs.LO↗

arXiv2012

High-frequency cyclicity in the Mediterranean Messinian evaporites: evidence for solar-lunar climate forcing

The deposition of varved sedimentary sequences is usually controlled by climate conditions. The study of two Late Miocene evaporite successions (one halite and the other gypsum) consisting of annual varves has been carried out to reconstruct the paleoclimatic and paleoenvironmental conditions existing during the acme of the Messinian salinity crisis, ~ 6 Ma, when thick evaporite deposits accumulated on the floor of the Mediterranean basin. Spectral analyses of these varved evaporitic successions reveal significant periodicity peaks at around 3-5, 9, 11-13, 20-27 and 50-100 yr. A comparison with modern precipitation data in the western Mediterranean shows that during the acme of the Messinian salinity crisis the climate was not in a permanent evaporitic stage, but in a dynamic situation where evaporite deposition was controlled by quasi-periodic climate oscillations with similarity to modern analogs including Quasi-Biennial Oscillation, El Niño Southern Oscillation, and decadal to secular lunar- and solar-induced cycles. Particularly we found a significant quasi-decadal oscillation with a prominent 9-year peak that is commonly found also in modern temperature records and is present in the contemporary Atlantic Multidecadal Oscillation (AMO) index and Pacific Decadal Oscillation (PDO) index. These cyclicities are common to both ancient and modern climate records because they can be associated with solar and solar-lunar tidal cycles.

physics.geo-ph↗

arXiv2012

Software Model Checking with Explicit Scheduler and Symbolic Threads

In many practical application domains, the software is organized into a set of threads, whose activation is exclusive and controlled by a cooperative scheduling policy: threads execute, without any interruption, until they either terminate or yield the control explicitly to the scheduler. The formal verification of such software poses significant challenges. On the one side, each thread may have infinite state space, and might call for abstraction. On the other side, the scheduling policy is often important for correctness, and an approach based on abstracting the scheduler may result in loss of precision and false positives. Unfortunately, the translation of the problem into a purely sequential software model checking problem turns out to be highly inefficient for the available technologies. We propose a software model checking technique that exploits the intrinsic structure of these programs. Each thread is translated into a separate sequential program and explored symbolically with lazy abstraction, while the overall verification is orchestrated by the direct execution of the scheduler. The approach is optimized by filtering the exploration of the scheduler with the integration of partial-order reduction. The technique, called ESST (Explicit Scheduler, Symbolic Threads) has been implemented and experimentally evaluated on a significant set of benchmarks. The results demonstrate that ESST technique is way more effective than software model checking applied to the sequentialized programs, and that partial-order reduction can lead to further performance improvements.

cs.LO↗

arXiv2012

Formalization and Validation of Safety-Critical Requirements

The validation of requirements is a fundamental step in the development process of safety-critical systems. In safety critical applications such as aerospace, avionics and railways, the use of formal methods is of paramount importance both for requirements and for design validation. Nevertheless, while for the verification of the design, many formal techniques have been conceived and applied, the research on formal methods for requirements validation is not yet mature. The main obstacles are that, on the one hand, the correctness of requirements is not formally defined; on the other hand that the formalization and the validation of the requirements usually demands a strong involvement of domain experts. We report on a methodology and a series of techniques that we developed for the formalization and validation of high-level requirements for safety-critical applications. The main ingredients are a very expressive formal language and automatic satisfiability procedures. The language combines first-order, temporal, and hybrid logic. The satisfiability procedures are based on model checking and satisfiability modulo theory. We applied this technology within an industrial project to the validation of railways requirements.

cs.SE↗