Showing 1–22 of 22 results for author: Lazic, R

Learning a Neuron by a Shallow ReLU Network: Dynamics and Implicit Bias for Correlated Inputs

Authors: Dmitry Chistikov, Matthias Englert, Ranko Lazic

Abstract: We prove that, for the fundamental regression task of learning a single neuron, training a one-hidden layer ReLU network of any width by gradient flow from a small initialisation converges to zero loss and is implicitly biased to minimise the rank of network parameters. By assuming that the training points are correlated with the teacher neuron, we complement previous work that considered orthogon… ▽ More We prove that, for the fundamental regression task of learning a single neuron, training a one-hidden layer ReLU network of any width by gradient flow from a small initialisation converges to zero loss and is implicitly biased to minimise the rank of network parameters. By assuming that the training points are correlated with the teacher neuron, we complement previous work that considered orthogonal datasets. Our results are based on a detailed non-asymptotic analysis of the dynamics of each hidden neuron throughout the training. We also show and characterise a surprising distinction in this setting between interpolator networks of minimal rank and those of minimal Euclidean norm. Finally we perform a range of numerical experiments, which corroborate our theoretical findings. △ Less

Submitted 1 October, 2023; v1 submitted 10 June, 2023; originally announced June 2023.

MSC Class: 68Q32; 68T07 ACM Class: I.2.6

Adversarial Reprogramming Revisited

Authors: Matthias Englert, Ranko Lazic

Abstract: Adversarial reprogramming, introduced by Elsayed, Goodfellow, and Sohl-Dickstein, seeks to repurpose a neural network to perform a different task, by manipulating its input without modifying its weights. We prove that two-layer ReLU neural networks with random weights can be adversarially reprogrammed to achieve arbitrarily high accuracy on Bernoulli data models over hypercube vertices, provided t… ▽ More Adversarial reprogramming, introduced by Elsayed, Goodfellow, and Sohl-Dickstein, seeks to repurpose a neural network to perform a different task, by manipulating its input without modifying its weights. We prove that two-layer ReLU neural networks with random weights can be adversarially reprogrammed to achieve arbitrarily high accuracy on Bernoulli data models over hypercube vertices, provided the network width is no greater than its input dimension. We also substantially strengthen a recent result of Phuong and Lampert on directional convergence of gradient flow, and obtain as a corollary that training two-layer ReLU neural networks on orthogonally separable datasets can cause their adversarial reprogramming to fail. We support these theoretical results by experiments that demonstrate that, as long as batch normalisation layers are suitably initialised, even untrained networks with random weights are susceptible to adversarial reprogramming. This is in contrast to observations in several recent works that suggested that adversarial reprogramming is not possible for untrained networks to any degree of reliability. △ Less

Submitted 11 October, 2022; v1 submitted 7 June, 2022; originally announced June 2022.

Human-like Relational Models for Activity Recognition in Video

Authors: Joseph Chrol-Cannon, Andrew Gilbert, Ranko Lazic, Adithya Madhusoodanan, Frank Guerin

Abstract: Video activity recognition by deep neural networks is impressive for many classes. However, it falls short of human performance, especially for challenging to discriminate activities. Humans differentiate these complex activities by recognising critical spatio-temporal relations among explicitly recognised objects and parts, for example, an object entering the aperture of a container. Deep neural… ▽ More Video activity recognition by deep neural networks is impressive for many classes. However, it falls short of human performance, especially for challenging to discriminate activities. Humans differentiate these complex activities by recognising critical spatio-temporal relations among explicitly recognised objects and parts, for example, an object entering the aperture of a container. Deep neural networks can struggle to learn such critical relationships effectively. Therefore we propose a more human-like approach to activity recognition, which interprets a video in sequential temporal phases and extracts specific relationships among objects and hands in those phases. Random forest classifiers are learnt from these extracted relationships. We apply the method to a challenging subset of the something-something dataset and achieve a more robust performance against neural network baselines on challenging activities. △ Less

Submitted 11 January, 2022; v1 submitted 12 July, 2021; originally announced July 2021.

Leafy Automata for Higher-Order Concurrency

Authors: Alex Dixon, Ranko Lazić, Andrzej S. Murawski, Igor Walukiewicz

Abstract: Finitary Idealized Concurrent Algol (FICA) is a prototypical programming language combining functional, imperative, and concurrent computation. There exists a fully abstract game model of FICA, which in principle can be used to prove equivalence and safety of FICA programs. Unfortunately, the problems are undecidable for the whole language, and only very rudimentary decidable sub-languages are kno… ▽ More Finitary Idealized Concurrent Algol (FICA) is a prototypical programming language combining functional, imperative, and concurrent computation. There exists a fully abstract game model of FICA, which in principle can be used to prove equivalence and safety of FICA programs. Unfortunately, the problems are undecidable for the whole language, and only very rudimentary decidable sub-languages are known. We propose leafy automata as a dedicated automata-theoretic formalism for representing the game semantics of FICA. The automata use an infinite alphabet with a tree structure. We show that the game semantics of any FICA term can be represented by traces of a leafy automaton. Conversely, the traces of any leafy automaton can be represented by a FICA term. Because of the close match with FICA, we view leafy automata as a promising starting point for finding decidable subclasses of the language and, more generally, to provide a new perspective on models of higher-order concurrent computation. Moreover, we identify a fragment of FICA that is amenable to verification by translation into a particular class of leafy automata. Using a locality property of the latter class, where communication between levels is restricted and every other level is bounded, we show that their emptiness problem is decidable by reduction to Petri net reachability. △ Less

Submitted 21 January, 2021; originally announced January 2021.

Comments: 18 pages plus appendices

Reachability in fixed dimension vector addition systems with states

Authors: Wojciech Czerwiński, Sławomir Lasota, Ranko Lazić, Jérôme Leroux, Filip Mazowiecki

Abstract: The reachability problem is a central decision problem for formal verification based on vector addition systems with states (VASS), which are equivalent to Petri nets and form one of the most studied and applied models of concurrency. Reachability for VASS is also inter-reducible with a plethora of problems from a number of areas of computer science. In spite of recent progress, the complexity of… ▽ More The reachability problem is a central decision problem for formal verification based on vector addition systems with states (VASS), which are equivalent to Petri nets and form one of the most studied and applied models of concurrency. Reachability for VASS is also inter-reducible with a plethora of problems from a number of areas of computer science. In spite of recent progress, the complexity of the reachability problem remains unsettled, and it is closely related to the lengths of shortest VASS runs that witness reachability. We consider VASS of fixed dimension, and obtain three main results. For the first two, we assume that the integers in the input are given in unary, and that the control graph of the given VASS is flat (i.e., without nested cycles). We obtain a family of VASS in dimension 3 whose shortest reachability witnessing runs are exponential, and we show that the reachability problem is NP-hard in dimension 7. These results resolve negatively questions that had been posed by the works of Blondin et al. in LICS 2015 and Englert et al. in LICS 2016, and contribute a first construction that distinguishes 3-dimensional flat VASS from 2-dimensional VASS. Our third result, by means of a novel family of products of integer fractions, shows that 4-dimensional VASS can have doubly exponentially long shortest reachability witnessing runs. The smallest dimension for which this was previously known is 14. △ Less

Submitted 10 May, 2020; v1 submitted 13 January, 2020; originally announced January 2020.

The Reachability Problem for Petri Nets is Not Elementary

Authors: Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jerome Leroux, Filip Mazowiecki

Abstract: Petri nets, also known as vector addition systems, are a long established model of concurrency with extensive applications in modelling and analysis of hardware, software and database systems, as well as chemical, biological and business processes. The central algorithmic problem for Petri nets is reachability: whether from the given initial configuration there exists a sequence of valid execution… ▽ More Petri nets, also known as vector addition systems, are a long established model of concurrency with extensive applications in modelling and analysis of hardware, software and database systems, as well as chemical, biological and business processes. The central algorithmic problem for Petri nets is reachability: whether from the given initial configuration there exists a sequence of valid execution steps that reaches the given final configuration. The complexity of the problem has remained unsettled since the 1960s, and it is one of the most prominent open questions in the theory of verification. Decidability was proved by Mayr in his seminal STOC 1981 work, and the currently best published upper bound is non-primitive recursive Ackermannian of Leroux and Schmitz from LICS 2019. We establish a non-elementary lower bound, i.e. that the reachability problem needs a tower of exponentials of time and space. Until this work, the best lower bound has been exponential space, due to Lipton in 1976. The new lower bound is a major breakthrough for several reasons. Firstly, it shows that the reachability problem is much harder than the coverability (i.e., state reachability) problem, which is also ubiquitous but has been known to be complete for exponential space since the late 1970s. Secondly, it implies that a plethora of problems from formal languages, logic, concurrent systems, process calculi and other areas, that are known to admit reductions from the Petri nets reachability problem, are also not elementary. Thirdly, it makes obsolete the currently best lower bounds for the reachability problems for two key extensions of Petri nets: with branching and with a pushdown stack. △ Less

Submitted 11 April, 2019; v1 submitted 19 September, 2018; originally announced September 2018.

Comments: Final version of STOC'19

Universal trees grow inside separating automata: Quasi-polynomial lower bounds for parity games

Authors: Wojciech Czerwiński, Laure Daviaud, Nathanaël Fijalkow, Marcin Jurdziński, Ranko Lazić, Paweł Parys

Abstract: Several distinct techniques have been proposed to design quasi-polynomial algorithms for solving parity games since the breakthrough result of Calude, Jain, Khoussainov, Li, and Stephan (2017): play summaries, progress measures and register games. We argue that all those techniques can be viewed as instances of the separation approach to solving parity games, a key technical component of which is… ▽ More Several distinct techniques have been proposed to design quasi-polynomial algorithms for solving parity games since the breakthrough result of Calude, Jain, Khoussainov, Li, and Stephan (2017): play summaries, progress measures and register games. We argue that all those techniques can be viewed as instances of the separation approach to solving parity games, a key technical component of which is constructing (explicitly or implicitly) an automaton that separates languages of words encoding plays that are (decisively) won by either of the two players. Our main technical result is a quasi-polynomial lower bound on the size of such separating automata that nearly matches the current best upper bounds. This forms a barrier that all existing approaches must overcome in the ongoing quest for a polynomial-time algorithm for solving parity games. The key and fundamental concept that we introduce and study is a universal ordered tree. The technical highlights are a quasi-polynomial lower bound on the size of universal ordered trees and a proof that every separating safety automaton has a universal tree hidden in its state space. △ Less

Submitted 2 November, 2018; v1 submitted 27 July, 2018; originally announced July 2018.

Comments: To appear in SODA 2019

When is Containment Decidable for Probabilistic Automata?

Authors: Laure Daviaud, Marcin Jurdziński, Ranko Lazić, Filip Mazowiecki, Guillermo A. Pérez, James Worrell

Abstract: The emptiness and containment problems for probabilistic automata are natural quantitative generalisations of the classical language emptiness and inclusion problems for Boolean automata. It is well known that both problems are undecidable. In this paper we provide a more refined view of these problems in terms of the degree of ambiguity of probabilistic automata. We show that a gap version of the… ▽ More The emptiness and containment problems for probabilistic automata are natural quantitative generalisations of the classical language emptiness and inclusion problems for Boolean automata. It is well known that both problems are undecidable. In this paper we provide a more refined view of these problems in terms of the degree of ambiguity of probabilistic automata. We show that a gap version of the emptiness problem (that is known be undecidable in general) becomes decidable for automata of polynomial ambiguity. We complement this positive result by showing that the emptiness problem remains undecidable even when restricted to automata of linear ambiguity. We then turn to finitely ambiguous automata. Here we show decidability of containment in case one of the automata is assumed to be unambiguous while the other one is allowed to be finitely ambiguous. Our proof of this last result relies on the decidability of the theory of real exponentiation, which has been shown, subject to Schanuel's Conjecture, by Macintyre and Wilkie. △ Less

Submitted 29 March, 2020; v1 submitted 24 April, 2018; originally announced April 2018.

ACM Class: F.3.1

A pseudo-quasi-polynomial algorithm for solving mean-payoff parity games

Authors: Laure Daviaud, Marcin Jurdzinski, Ranko Lazic

Abstract: In a mean-payoff parity game, one of the two players aims both to achieve a qualitative parity objective and to minimize a quantitative long-term average of payoffs (aka. mean payoff). The game is zero-sum and hence the aim of the other player is to either foil the parity objective or to maximize the mean payoff. Our main technical result is a pseudo-quasi-polynomial algorithm for solving mean-p… ▽ More In a mean-payoff parity game, one of the two players aims both to achieve a qualitative parity objective and to minimize a quantitative long-term average of payoffs (aka. mean payoff). The game is zero-sum and hence the aim of the other player is to either foil the parity objective or to maximize the mean payoff. Our main technical result is a pseudo-quasi-polynomial algorithm for solving mean-payoff parity games. All algorithms for the problem that have been developed for over a decade have a pseudo-polynomial and an exponential factors in their running times; in the running time of our algorithm the latter is replaced with a quasi-polynomial one. By the results of Chatterjee and Doyen (2012) and of Schewe, Weinert, and Zimmermann (2018), our main technical result implies that there are pseudo-quasi-polynomial algorithms for solving parity energy games and for solving parity games with weights. Our main conceptual contributions are the definitions of strategy decompositions for both players, and a notion of progress measures for mean-payoff parity games that generalizes both parity and energy progress measures. The former provides normal forms for and succinct representations of winning strategies, and the latter enables the application to mean-payoff parity games of the order-theoretic machinery that underpins a recent quasi-polynomial algorithm for solving parity games. △ Less

Submitted 10 July, 2018; v1 submitted 13 March, 2018; originally announced March 2018.

Perfect Half Space Games

Authors: Thomas Colcombet, Marcin Jurdziński, Ranko Lazić, Sylvain Schmitz

Abstract: We introduce perfect half space games, in which the goal of Player 2 is to make the sums of encountered multi-dimensional weights diverge in a direction which is consistent with a chosen sequence of perfect half spaces (chosen dynamically by Player 2). We establish that the bounding games of Jurdziński et al. (ICALP 2015) can be reduced to perfect half space games, which in turn can be translated… ▽ More We introduce perfect half space games, in which the goal of Player 2 is to make the sums of encountered multi-dimensional weights diverge in a direction which is consistent with a chosen sequence of perfect half spaces (chosen dynamically by Player 2). We establish that the bounding games of Jurdziński et al. (ICALP 2015) can be reduced to perfect half space games, which in turn can be translated to the lexicographic energy games of Colcombet and Niwiński, and are positionally determined in a strong sense (Player 2 can play without knowing the current perfect half space). We finally show how perfect half space games and bounding games can be employed to solve multi-dimensional energy parity games in pseudo-polynomial time when both the numbers of energy dimensions and of priorities are fixed, regardless of whether the initial credit is given as part of the input or existentially quantified. This also yields an optimal 2-EXPTIME complexity with given initial credit, where the best known upper bound was non-elementary. △ Less

Submitted 20 April, 2017; v1 submitted 19 April, 2017; originally announced April 2017.

Comments: Accepted at LICS 2017

Journal ref: 32nd Annual ACM/IEEE Symposium on Logic In Computer Science (LICS 2017)

Succinct progress measures for solving parity games

Authors: Marcin Jurdzinski, Ranko Lazic

Abstract: The recent breakthrough paper by Calude et al. has given the first algorithm for solving parity games in quasi-polynomial time, where previously the best algorithms were mildly subexponential. We devise an alternative quasi-polynomial time algorithm based on progress measures, which allows us to reduce the space required from quasi-polynomial to nearly linear. Our key technical tools are a novel c… ▽ More The recent breakthrough paper by Calude et al. has given the first algorithm for solving parity games in quasi-polynomial time, where previously the best algorithms were mildly subexponential. We devise an alternative quasi-polynomial time algorithm based on progress measures, which allows us to reduce the space required from quasi-polynomial to nearly linear. Our key technical tools are a novel concept of ordered tree coding, and a succinct tree coding result that we prove using bounded adaptive multi-counters, both of which are interesting in their own right. △ Less

Submitted 4 April, 2018; v1 submitted 16 February, 2017; originally announced February 2017.

A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One

Authors: Stefan Göller, Christoph Haase, Ranko Lazić, Patrick Totzke

Abstract: Branching VASS (BVASS) generalise vector addition systems with states by allowing for special branching transitions that can non-deterministically distribute a counter value between two control states. A run of a BVASS consequently becomes a tree, and reachability is to decide whether a given configuration is the root of a reachability tree. This paper shows P-completeness of reachability in BVASS… ▽ More Branching VASS (BVASS) generalise vector addition systems with states by allowing for special branching transitions that can non-deterministically distribute a counter value between two control states. A run of a BVASS consequently becomes a tree, and reachability is to decide whether a given configuration is the root of a reachability tree. This paper shows P-completeness of reachability in BVASS in dimension one, the first decidability result for reachability in a subclass of BVASS known so far. Moreover, we show that coverability and boundedness in BVASS in dimension one are P-complete as well. △ Less

Submitted 6 May, 2016; v1 submitted 17 February, 2016; originally announced February 2016.

Reachability in Two-Dimensional Unary Vector Addition Systems with States is NL-Complete

Authors: Matthias Englert, Ranko Lazić, Patrick Totzke

Abstract: Blondin et al. showed at LICS 2015 that two-dimensional vector addition systems with states have reachability witnesses of length exponential in the number of states and polynomial in the norm of vectors. The resulting guess-and-verify algorithm is optimal (PSPACE), but only if the input vectors are given in binary. We answer positively the main question left open by their work, namely establish t… ▽ More Blondin et al. showed at LICS 2015 that two-dimensional vector addition systems with states have reachability witnesses of length exponential in the number of states and polynomial in the norm of vectors. The resulting guess-and-verify algorithm is optimal (PSPACE), but only if the input vectors are given in binary. We answer positively the main question left open by their work, namely establish that reachability witnesses of pseudo-polynomial length always exist. Hence, when the input vectors are given in unary, the improved guess-and-verify algorithm requires only logarithmic space. △ Less

Submitted 6 May, 2016; v1 submitted 1 February, 2016; originally announced February 2016.

ACM Class: F.1.1

Fixed-Dimensional Energy Games are in Pseudo-Polynomial Time

Authors: Marcin Jurdziński, Ranko Lazić, Sylvain Schmitz

Abstract: We generalise the hyperplane separation technique (Chatterjee and Velner, 2013) from multi-dimensional mean-payoff to energy games, and achieve an algorithm for solving the latter whose running time is exponential only in the dimension, but not in the number of vertices of the game graph. This answers an open question whether energy games with arbitrary initial credit can be solved in pseudo-polyn… ▽ More We generalise the hyperplane separation technique (Chatterjee and Velner, 2013) from multi-dimensional mean-payoff to energy games, and achieve an algorithm for solving the latter whose running time is exponential only in the dimension, but not in the number of vertices of the game graph. This answers an open question whether energy games with arbitrary initial credit can be solved in pseudo-polynomial time for fixed dimensions 3 or larger (Chaloupka, 2013). It also improves the complexity of solving multi-dimensional energy games with given initial credit from non-elementary (Brázdil, Jančar, and Kučera, 2010) to 2EXPTIME, thus establishing their 2EXPTIME-completeness. △ Less

Submitted 6 September, 2021; v1 submitted 24 February, 2015; originally announced February 2015.

Comments: Corrected proofs in former Section 3.3 Energy Games with Given Initial Credit

Journal ref: Proceedings of ICALP 2015, Lecture Notes in Computer Science vol. 9135, pp. 260--272, Springer

Non-Elementary Complexities for Branching VASS, MELL, and Extensions

Authors: Ranko Lazić, Sylvain Schmitz

Abstract: We study the complexity of reachability problems on branching extensions of vector addition systems, which allows us to derive new non-elementary complexity bounds for fragments and variants of propositional linear logic. We show that provability in the multiplicative exponential fragment is Tower-hard already in the affine case -- and hence non-elementary. We match this lower bound for the full p… ▽ More We study the complexity of reachability problems on branching extensions of vector addition systems, which allows us to derive new non-elementary complexity bounds for fragments and variants of propositional linear logic. We show that provability in the multiplicative exponential fragment is Tower-hard already in the affine case -- and hence non-elementary. We match this lower bound for the full propositional affine linear logic, proving its Tower-completeness. We also show that provability in propositional contractive linear logic is Ackermann-complete. △ Less

Submitted 16 May, 2022; v1 submitted 27 January, 2014; originally announced January 2014.

Comments: Fixed Fig. 3 thanks to Hiromi Tanaka

ACM Class: F.2.2; F.4.1

Journal ref: ACM Transactions on Computational Logic, vol. 16, issue 3, article 20, 2015

The reachability problem for vector addition systems with a stack is not elementary

Authors: Ranko Lazic

Abstract: By adapting the iterative yardstick construction of Stockmeyer, we show that the reachability problem for vector addition systems with a stack does not have elementary complexity. As a corollary, the same lower bound holds for the satisfiability problem for a two-variable first-order logic on trees in which unbounded data may label only leaf nodes. Whether the two problems are decidable remains an… ▽ More By adapting the iterative yardstick construction of Stockmeyer, we show that the reachability problem for vector addition systems with a stack does not have elementary complexity. As a corollary, the same lower bound holds for the satisfiability problem for a two-variable first-order logic on trees in which unbounded data may label only leaf nodes. Whether the two problems are decidable remains an open question. △ Less

Submitted 7 October, 2013; originally announced October 2013.

Comments: Informal presentation, 6th International Workshop on Reachability Problems (RP), Bordeaux, September 2012

ACM Class: F.3.1; F.4.3

Model checking memoryful linear-time logics over one-counter automata

Authors: Stephane Demri, Ranko Lazic, Arnaud Sangnier

Abstract: We study complexity of the model-checking problems for LTL with registers (also known as freeze LTL) and for first-order logic with data equality tests over one-counter automata. We consider several classes of one-counter automata (mainly deterministic vs. nondeterministic) and several logical fragments (restriction on the number of registers or variables and on the use of propositional variable… ▽ More We study complexity of the model-checking problems for LTL with registers (also known as freeze LTL) and for first-order logic with data equality tests over one-counter automata. We consider several classes of one-counter automata (mainly deterministic vs. nondeterministic) and several logical fragments (restriction on the number of registers or variables and on the use of propositional variables for control locations). The logics have the ability to store a counter value and to test it later against the current counter value. We show that model checking over deterministic one-counter automata is PSPACE-complete with infinite and finite accepting runs. By constrast, we prove that model checking freeze LTL in which the until operator is restricted to the eventually operator over nondeterministic one-counter automata is undecidable even if only one register is used and with no propositional variable. As a corollary of our proof, this also holds for first-order logic with data equality tests restricted to two variables. This makes a difference with the facts that several verification problems for one-counter automata are known to be decidable with relatively low complexity, and that finitary satisfiability for the two logics are decidable. Our results pave the way for model-checking memoryful (linear-time) logics over other classes of operational models, such as reversal-bounded counter machines. △ Less

Submitted 18 January, 2010; v1 submitted 30 October, 2008; originally announced October 2008.

Comments: Substantially revised and extended version of "Model checking freeze LTL over one-counter automata" by the same authors in FoSSaCS 2008

ACM Class: F.1.1; F.4.1

Alternating Automata on Data Trees and XPath Satisfiability

Authors: Marcin Jurdzinski, Ranko Lazic

Abstract: A data tree is an unranked ordered tree whose every node is labelled by a letter from a finite alphabet and an element ("datum") from an infinite set, where the latter can only be compared for equality. The article considers alternating automata on data trees that can move downward and rightward, and have one register for storing data. The main results are that nonemptiness over finite data trees… ▽ More A data tree is an unranked ordered tree whose every node is labelled by a letter from a finite alphabet and an element ("datum") from an infinite set, where the latter can only be compared for equality. The article considers alternating automata on data trees that can move downward and rightward, and have one register for storing data. The main results are that nonemptiness over finite data trees is decidable but not primitive recursive, and that nonemptiness of safety automata is decidable but not elementary. The proofs use nondeterministic tree automata with faulty counters. Allowing upward moves, leftward moves, or two registers, each causes undecidability. As corollaries, decidability is obtained for two data-sensitive fragments of the XPath query language. △ Less

Submitted 14 June, 2010; v1 submitted 2 May, 2008; originally announced May 2008.

Comments: 23 pages

ACM Class: F.4.1; F.1.1; H.2.3

Safety alternating automata on data words

Authors: Ranko Lazic

Abstract: A data word is a sequence of pairs of a letter from a finite alphabet and an element from an infinite set, where the latter can only be compared for equality. Safety one-way alternating automata with one register on infinite data words are considered, their nonemptiness is shown EXPSPACE-complete, and their inclusion decidable but not primitive recursive. The same complexity bounds are obtained… ▽ More A data word is a sequence of pairs of a letter from a finite alphabet and an element from an infinite set, where the latter can only be compared for equality. Safety one-way alternating automata with one register on infinite data words are considered, their nonemptiness is shown EXPSPACE-complete, and their inclusion decidable but not primitive recursive. The same complexity bounds are obtained for satisfiability and refinement, respectively, for the safety fragment of linear temporal logic with freeze quantification. Drop** the safety restriction, adding past temporal operators, or adding one more register, each causes undecidability. △ Less

Submitted 9 April, 2010; v1 submitted 28 February, 2008; originally announced February 2008.

Comments: 23 pages

ACM Class: F.4.1; F.1.1

LTL with the Freeze Quantifier and Register Automata

Authors: Stephane Demri, Ranko Lazic

Abstract: A data word is a sequence of pairs of a letter from a finite alphabet and an element from an infinite set, where the latter can only be compared for equality. To reason about data words, linear temporal logic is extended by the freeze quantifier, which stores the element at the current word position into a register, for equality comparisons deeper in the formula. By translations from the logic t… ▽ More A data word is a sequence of pairs of a letter from a finite alphabet and an element from an infinite set, where the latter can only be compared for equality. To reason about data words, linear temporal logic is extended by the freeze quantifier, which stores the element at the current word position into a register, for equality comparisons deeper in the formula. By translations from the logic to alternating automata with registers and then to faulty counter automata whose counters may erroneously increase at any time, and from faulty and error-free counter automata to the logic, we obtain a complete complexity table for logical fragments defined by varying the set of temporal operators and the number of registers. In particular, the logic with future-time operators and 1 register is decidable but not primitive recursive over finite data words. Adding past-time operators or 1 more register, or switching to infinite data words, cause undecidability. △ Less

Submitted 3 April, 2008; v1 submitted 5 October, 2006; originally announced October 2006.

Comments: 29 pages

ACM Class: F.1.1; F.4.1

On the freeze quantifier in Constraint LTL: decidability and complexity

Authors: Stéphane Demri, Ranko Lazic, David Nowak

Abstract: Constraint LTL, a generalisation of LTL over Presburger constraints, is often used as a formal language to specify the behavior of operational models with constraints. The freeze quantifier can be part of the language, as in some real-time logics, but this variable-binding mechanism is quite general and ubiquitous in many logical languages (first-order temporal logics, hybrid logics, logics for… ▽ More Constraint LTL, a generalisation of LTL over Presburger constraints, is often used as a formal language to specify the behavior of operational models with constraints. The freeze quantifier can be part of the language, as in some real-time logics, but this variable-binding mechanism is quite general and ubiquitous in many logical languages (first-order temporal logics, hybrid logics, logics for sequence diagrams, navigation logics, logics with lambda-abstraction etc.). We show that Constraint LTL over the simple domain (N,=) augmented with the freeze quantifier is undecidable which is a surprising result in view of the poor language for constraints (only equality tests). Many versions of freeze-free Constraint LTL are decidable over domains with qualitative predicates and our undecidability result actually establishes Sigma_1^1-completeness. On the positive side, we provide complexity results when the domain is finite (EXPSPACE-completeness) or when the formulae are flat in a sense introduced in the paper. Our undecidability results are sharp (i.e. with restrictions on the number of variables) and all our complexity characterisations ensure completeness with respect to some complexity class (mainly PSPACE and EXPSPACE). △ Less

Submitted 29 September, 2006; v1 submitted 4 September, 2006; originally announced September 2006.

Comments: 29 pages

Journal ref: Information and Computation, 205(1):2-24, January 2007

On model checking data-independent systems with arrays without reset

Authors: R. S. Lazic, T. C. Newcomb, A. W. Roscoe

Abstract: A system is data-independent with respect to a data type X iff the operations it can perform on values of type X are restricted to just equality testing. The system may also store, input and output values of type X. We study model checking of systems which are data-independent with respect to two distinct type variables X and Y, and may in addition use arrays with indices from X and values from… ▽ More A system is data-independent with respect to a data type X iff the operations it can perform on values of type X are restricted to just equality testing. The system may also store, input and output values of type X. We study model checking of systems which are data-independent with respect to two distinct type variables X and Y, and may in addition use arrays with indices from X and values from Y . Our main interest is the following parameterised model-checking problem: whether a given program satisfies a given temporal-logic formula for all non-empty nite instances of X and Y . Initially, we consider instead the abstraction where X and Y are infinite and where partial functions with finite domains are used to model arrays. Using a translation to data-independent systems without arrays, we show that the u-calculus model-checking problem is decidable for these systems. From this result, we can deduce properties of all systems with finite instances of X and Y . We show that there is a procedure for the above parameterised model-checking problem of the universal fragment of the u-calculus, such that it always terminates but may give false negatives. We also deduce that the parameterised model-checking problem of the universal disjunction-free fragment of the u-calculus is decidable. Practical motivations for model checking data-independent systems with arrays include verification of memory and cache systems, where X is the type of memory addresses, and Y the type of storable values. As an example we verify a fault-tolerant memory interface over a set of unreliable memories. △ Less

Submitted 26 May, 2004; originally announced May 2004.

Comments: Appeared in Theory and Practice of Logic Programming, vol. 4, no. 5&6, 2004

ACM Class: D.1.6; D.3.2

Journal ref: Theory and Practice of Logic Programming, vol. 4, no. 5&6, 2004