113 citations · 260 across the 57 of their papers we have counts for
23 papers · 1 filter
On Variable-Bounded Non-Linear Expansions of Presburger Arithmetic
Piotr Bacik, Joris Nieuwveld, Joël Ouaknine +3
We consider expansions of Presburger arithmetic with families of monadic polynomial predicates. (Examples of such predicates are the set of perfect squares, or the set of integers…
The 2-Dimensional Constraint Loop Problem is Decidable
Quentin Guilmant, Engel Lefaucheux, Joël Ouaknine +1
A linear constraint loop is specified by a system of linear inequalities that define the relation between the values of the program variables before and after a single execution of…
Multiple Reachability in Linear Dynamical Systems
Toghrul Karimov, Edon Kelmendi, Joël Ouaknine +1
We consider reachability decision problems for linear dynamical systems: Given a linear map on , together with source and target sets, determine whether there is a p…
Model Checking Linear Dynamical Systems under Floating-point Rounding
Engel Lefaucheux, Joël Ouaknine, David Purser +1
We consider linear dynamical systems under floating-point rounding. In these systems, a matrix is repeatedly applied to a vector, but the numbers are rounded into floating-point re…
The Pseudo-Reachability Problem for Diagonalisable Linear Dynamical Systems
Julian D'Costa, Toghrul Karimov, Rupak Majumdar +3
We study fundamental reachability problems on pseudo-orbits of linear dynamical systems. Pseudo-orbits can be viewed as a model of computation with limited precision and pseudo-rea…
Porous Invariants
Engel Lefaucheux, Joël Ouaknine, David Purser +1
We introduce the notion of porous invariants for multipath (or branching/nondeterministic) affine loops over the integers; these invariants are not necessarily convex, and can in f…
The Orbit Problem for Parametric Linear Dynamical Systems
Christel Baier, Florian Funke, Simon Jantsch +7
We study a parametric version of the Kannan-Lipton Orbit Problem for linear dynamical systems. We show decidability in the case of one parameter and Skolem-hardness with two or mor…
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…
On LTL Model Checking for Low-Dimensional Discrete Linear Dynamical Systems
Toghrul Karimov, Joël Ouaknine, James Worrell
Consider a discrete dynamical system given by a square matrix and a starting point . The orbit of such a system is the infinite…
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…
On the Monniaux Problem in Abstract Interpretation
Nathanaël Fijalkow, Engel Lefaucheux, Pierre Ohlmann +3
The Monniaux Problem in abstract interpretation asks, roughly speaking, whether the following question is decidable: given a program , a safety (\emph{e.g.}, non-reachability) s…
Sequential Relational Decomposition
Dror Fried, Axel Legay, Joël Ouaknine +1
The concept of decomposition in computer science and engineering is considered a fundamental component of computational thinking and is prevalent in design of algorithms, software…
Algebraic Invariants for Linear Hybrid Automata
Rupak Majumdar, Joël Ouaknine, Amaury Pouly +1
We exhibit an algorithm to compute the strongest algebraic (or polynomial) invariants that hold at each location of a given unguarded linear hybrid automaton (i.e., a hybrid automa…
On the Expressiveness and Monitoring of Metric Temporal Logic
Hsi-Ming Ho, Joël Ouaknine, James Worrell
It is known that Metric Temporal Logic (MTL) is strictly less expressive than the Monadic First-Order Logic of Order and Metric (FO[<, +1]) when interpreted over timed words; this…
Polynomial Invariants for Affine Programs
Ehud Hrushovski, Joël Ouaknine, Amaury Pouly +1
We exhibit an algorithm to compute the strongest polynomial (or algebraic) invariants that hold at each location of a given affine program (i.e., a program having only non-determin…
Model Checking Flat Freeze LTL on One-Counter Automata
Antonia Lechner, Richard Mayr, Joël Ouaknine +2
Freeze LTL is a temporal logic with registers that is suitable for specifying properties of data words. In this paper we study the model checking problem for Freeze LTL on one-coun…
The Cyclic-Routing UAV Problem is PSPACE-Complete
Hsi-Ming Ho, Joel Ouaknine
Consider a finite set of targets, with each target assigned a relative deadline, and each pair of targets assigned a fixed transit flight time. Given a flock of identical UAVs, can…
On the Complexity of Temporal-Logic Path Checking
Daniel Bundala, Joël Ouaknine
Given a formula in a temporal logic such as LTL or MTL, a fundamental problem is the complexity of evaluating the formula on a given finite word. For LTL, the complexity of this ta…
A Static Analysis Framework for Livelock Freedom in CSP
Joel Ouaknine, Hristina Palikareva, A. W. Roscoe +1
In a process algebra with hiding and recursion it is possible to create processes which compute internally without ever communicating with their environment. Such processes are sai…
Time-bounded Reachability for Hybrid Automata: Complexity and Fixpoints
Thomas Brihaye, Laurent Doyen, Gilles Geeraerts +3
In this paper, we study thetime-bounded reachability problem for rectangular hybrid automata with non-negative rates (RHA+). This problem was recently shown to be decidable [Brihay…
Expressive Completeness of Metric Temporal Logic
Paul Hunter, Joël Ouaknine, James Worrell
Metric Temporal Logic (MTL) is a generalisation of Linear Temporal Logic in which the Until and Since modalities are annotated with intervals that express metric constraints. A sem…
On Reachability for Hybrid Automata over Bounded Time
Thomas Brihaye, Laurent Doyen, Gilles Geeraerts +3
This paper investigates the time-bounded version of the reachability problem for hybrid automata. This problem asks whether a given hybrid automaton can reach a given target locati…
On the decidability and complexity of Metric Temporal Logic over finite words
Joel Ouaknine, James Worrell
Metric Temporal Logic (MTL) is a prominent specification formalism for real-time systems. In this paper, we show that the satisfiability problem for MTL over finite timed words is…