Search

Maxmin-$\omega$ dynamical systems were previously introduced as a generalization of dynamical systems expressed by tropical linear algebra. To describe steady states of such systems one has to study an eigenproblem of the form $A\otimes_{\omega} x=\lambda+x$ where $\otimes_{\omega}$ is the maxmin-$\omega$ matrix-vector multiplication. This eigenproblem can be viewed in more general framework of nonlinear Perron-Frobenius theory. However, instead of studying such eigenspaces directly we develop a different approach: over-approximation by zones. These are traditionally convex sets of special kind which proved to be highly useful in computer science and also relevant in tropical convexity. We first construct a sequence of zones over-approximating a maxmin-$\omega$ eigenspace. Next, the limit of this sequence is refined in a heuristic procedure, which yields a refined zone and also the eigenvalue $\lambda$ with a high success rate. Based on the numerical experiments, in successful cases there is a column of the difference bound matrix (DBM) representation of the refined zone which yields an eigenvector., Comment: 21 pages

Max-Plus Linear (MPL) systems are an algebraic formalism with practical applications in transportation networks, manufacturing and biological systems. In this paper, we investigate the problem of automatically analyzing the properties of MPL, taking into account both structural properties such as transient and cyclicity, and the open problem of user-defined temporal properties. We propose Time-Difference LTL (TDLTL), a logic that encompasses the delays between the discrete time events governed by an MPL system, and characterize the problem of model checking TDLTL over MPL. We first consider a framework based on the verification of infinite-state transition systems, and propose an approach based on an encoding into model checking. Then, we leverage the specific features of MPL systems to devise a highly optimized, combinational approach based on Satisfiability Modulo Theory (SMT). We experimentally evaluate the features of the proposed approaches on a large set of benchmarks. The results show that the proposed approach substantially outperforms the state of the art competitors in expressiveness and effectiveness, and demonstrate the superiority of the combinational approach over the reduction to model checking., Comment: 28 pages (including appendixes)

Maxmin-$\omega$ dynamical systems were previously introduced as an ``all-in-one package'' that can yield a solely min-plus, a solely max-plus, or a max-min-plus dynamical system by varying a parameter $\omega\in(0,1]$. With such systems in mind, it is natural to introduce and consider maxmin-$\omega$ linear systems of equations of the type $A\otimes_{\omega} x=b$. However, to our knowledge, such maxmin-$\omega$ linear systems have not been studied before and in this paper we present an approach to solve them. We show that the problem can be simplified by performing normalization and then generating a ``canonical'' matrix which we call the principal order matrix. Instead of directly trying to find the solutions, we search the possible solution indices which can be identified using the principal order matrix and the parameter $\omega$. The fully active solutions are then immediately obtained from these solution indices. With the fully active solutions at hand, we then present the method to find other solutions by applying a relaxation, i.e., increasing or decreasing some components of fully active solutions. This approach can be seen as a generalization of an approach that could be applied to solve max-plus or min-plus linear systems. Our results also shed more light on an unusual feature of maxmin-$\omega$ linear systems, which, unlike in the usual linear algebra, can have a finite number of solutions in the case where their solution is non-unique., Comment: 17 pages

This work discusses the reachability analysis (RA) of Max-Plus Linear (MPL) systems, a class of continuous-space, discrete-event models defined over the max-plus algebra. Given the initial and target sets, we develop algorithms to verify whether there exist trajectories of the MPL system that, starting from the initial set, eventually reach the target set. We show that RA can be solved symbolically by encoding the MPL system, as well as initial and target sets into difference logic, and then checking the satisfaction of the resulting logical formula via an off-the-shelf satisfiability modulo theories (SMT) solver. The performance and scalability of the developed SMT-based algorithms are shown to clearly outperform state-of-the-art RA algorithms for MPL systems, newly allowing to investigate RA of high-dimensional MPL systems: the verification of models with more than 100 continuous variables shows the applicability of these techniques to MPL systems of industrial relevance., Comment: 7 pages, accepted in International Workshop on Discrete Event Systems (WODES) 2020

This paper proposes a new approach, grounded in Satisfiability Modulo Theories (SMT), to study the transient of a Max-Plus Linear (MPL) system, that is the number of steps leading to its periodic regime. Differently from state-of-the-art techniques, our approach allows the analysis of periodic behaviors for subsets of initial states, as well as the characterization of sets of initial states exhibiting the same specific periodic behavior and transient. Our experiments show that the proposed technique dramatically outperforms state-of-the-art methods based on max-plus algebra computations for systems of large dimensions., Comment: The paper consists of 22 pages (including references and Appendix). It is accepted in FORMATS 2020 First revision

This paper introduces the abstraction of max-plus linear (MPL) systems via predicates. Predicates are automatically selected from system matrix, as well as from the specifications under consideration. We focus on verifying time-difference specifications, which encompass the relation between successive events in MPL systems. We implement a bounded model checking (BMC) procedure over a predicate abstraction of the given MPL system, to verify the satisfaction of time-difference specifications. Our predicate abstractions are experimentally shown to improve on existing MPL abstractions algorithms. Furthermore, with focus on the BMC algorithm, we can provide an explicit upper bound on the completeness threshold by means of the transient and the cyclicity of the underlying MPL system., Comment: 19 pages, accepted in FORMATS 19

This paper describes the development of finite abstractions of Max-Plus-Linear (MPL) systems using tropical operations. The idea of tropical abstraction is inspired by the fact that an MPL system is a discrete-event model updating its state with operations in the tropical algebra. The abstract model is a finite-state transition system: we show that the abstract states can be generated by operations on the tropical algebra, and that the generation of transitions can be established by tropical multiplications of matrices. The complexity of the algorithms based on tropical algebra is discussed and their performance is tested on a numerical benchmark against an existing alternative abstraction approach., Comment: 20 pages including 5 pages Appendix. The paper is accepted in FORMATS'2018. We submit the longer version