| Resumo: | <p>Max-Plus Linear (MPL) systems are the class of discrete-event systems (DES) with
dynamics based on two binary operations (maximisation and addition) over the
so-called max-plus semiring. In practical applications, MPL systems are used to
model synchronisation phenomena without concurrency. Such are widely used in
railway networks, manufacturing plants, and modelling and studying biological systems. The dual of MPL systems is Min-Plus Linear (MiPL) systems which use
minimisation and addition operations. Furthermore, as a natural extension, Interval
Max-Plus Linear (IMPL) systems are MPL systems where real-valued intervals
characterise the delays between successive discrete events. In general, IMPL systems are more realistic than simple MPL ones. For instance, in a model of a railway network, the travel between two stations may take longer (or possibly faster) than the expected time due to unforeseen external factors such as weather conditions, driver’s behaviour, and the number of departing passengers at stations. The fundamental problems for the systems mentioned above are reachability analysis and formal verification, respectively assessing whether the dynamics of the underlying system eventually reaches a particular set and satisfies the intended specifications or requirements. The state-of-the-art approaches to tackle these problems employ the abstraction technique by leveraging the translation of an MPL (including MiPL and IMPL) system into an equivalent Piecewise Affine (PWA) system and using Difference-Bound Matrix (DBM) to express the resulting abstract states as well as the set of atomic propositions. Such an abstraction technique results in an abstract transition system that allows replacing the verification of specifications over the original model. However, the existing techniques are not complete since they cannot determine whether the counterexample found on the abstract transition system is spurious. The other disadvantages are related to the scalability of the abstraction procedure and the limited expressiveness of DBM when dealing with specifications that contain conjunction or negation. This work addresses these issues by proposing novel abstraction procedures by identifying the propositions from the underlying model and specifications before generating the abstract states. These novel approaches allow the verification of more expressive specifications in Linear Temporal Logic (LTL). In addition to this, using the Bounded Model Checking (BMC) algorithm combined with spuriousness checking (of counterexample) and refinement procedures, we present the complete verification framework where the corresponding completeness threshold is related to the periodic behaviour of the model. Such behaviour is determined by a pair of transient (i.e., the starting index of periodic behaviour) and cyclicity (also called periodicity). Despite these developments, the proposed abstraction-based procedures remain not scalable. We then propose alternative methods utilising Satisfiability Modulo Theory (SMT). The main idea underpinning the SMT-based methods is to transform the dynamics of the model and possibly the specifications under consideration into a formula in quantifier-free Real Difference Logic (QF-RDL) or Linear Real Arithmetics (QF-LRA). The satisfaction of the resulting formula, which can be checked by SMT solvers, corresponds to the output for reachability and verification problems. Finally, the performance of the proposed methods (abstraction-based and SMT-based) is evaluated via a set of computational benchmarks, where we observe a significant improvement for the SMT-based procedures w.r.t. the scalability, compared to existing approaches whenever available.</p>
|
|---|