54 citations · 95 across the 24 of their papers we have counts for
7 papers · 1 filter
The Geometry of Reachability in Continuous Vector Addition Systems with States
Shaull Almagor, Arka Ghosh, Tim Leys +1
We study the geometry of reachability sets of continuous vector addition systems with states (VASS). In particular we establish that they are almost Minkowski sums of convex cones…
Deciding -Regular Properties on Linear Recurrence Sequences
Shaull Almagor, Toghrul Karimov, Edon Kelmendi +2
We consider the problem of deciding -regular properties on infinite traces produced by linear loops. Here we think of a given loop as producing a single infinite trace that enco…
Process Symmetry in Probabilistic Transducers
Shaull Almagor
Model checking is the process of deciding whether a system satisfies a given specification. Often, when the setting comprises multiple processes, the specifications are over sets o…
Invariants for Continuous Linear Dynamical Systems
Shaull Almagor, Edon Kelmendi, Joël Ouaknine +1
Continuous linear dynamical systems are used extensively in mathematics, computer science, physics, and engineering to model the evolution of a system over time. A central techniqu…
Coverability in 1-VASS with Disequality Tests
Shaull Almagor, Nathann Cohen, Guillermo A. Pérez +2
We study a class of reachability problems in weighted graphs with constraints on the accumulated weight of paths. The problems we study can equivalently be formulated in the model…
High-Quality Synthesis Against Stochastic Environments
Shaull Almagor, Orna Kupferman
In the classical synthesis problem, we are given an LTL formula psi over sets of input and output signals, and we synthesize a transducer that realizes psi. One weakness of automat…
Discounting in LTL
Shaull Almagor, Udi Boker, Orna Kupferman
In recent years, there is growing need and interest in formalizing and reasoning about the quality of software and hardware systems. As opposed to traditional verification, where o…