-
Weighted basic parallel processes and combinatorial enumeration
Authors:
Lorenzo Clemente
Abstract:
We study weighted basic parallel processes (WBPP), a nonlinear recursive generalisation of weighted finite automata inspired from process algebra and Petri net theory. Our main result is an algorithm of 2-EXPSPACE complexity for the WBPP equivalence problem. While (unweighted) BPP language equivalence is undecidable, we can use this algorithm to decide multiplicity equivalence of BPP and language…
▽ More
We study weighted basic parallel processes (WBPP), a nonlinear recursive generalisation of weighted finite automata inspired from process algebra and Petri net theory. Our main result is an algorithm of 2-EXPSPACE complexity for the WBPP equivalence problem. While (unweighted) BPP language equivalence is undecidable, we can use this algorithm to decide multiplicity equivalence of BPP and language equivalence of unambiguous BPP, with the same complexity. These are long-standing open problems for the related model of weighted context-free grammars. Our second contribution is a connection between WBPP, power series solutions of systems of polynomial differential equations, and combinatorial enumeration. To this end we consider constructible differentially finite power series (CDF), a class of multivariate differentially algebraic series introduced by Bergeron and Reutenauer in order to provide a combinatorial interpretation to differential equations. CDF series generalise rational, algebraic, and a large class of D-finite (holonomic) series, for which decidability of equivalence was an open problem. We show that CDF series correspond to commutative WBPP series. As a consequence of our result on WBPP and commutativity, we show that equivalence of CDF power series can be decided with 2-EXPTIME complexity. The complexity analysis is based on effective bounds from algebraic geometry, namely on the length of chains of polynomial ideals constructed by repeated application of finitely many, not necessarily commuting derivations of a multivariate polynomial ring. This is obtained by generalising a result of Novikov and Yakovenko in the case of a single derivation, which is noteworthy since generic bounds on ideal chains are non-primitive recursive in general. On the way, we develop the theory of \WBPP~series and \CDF~power series, exposing several of their appealing properties.
△ Less
Submitted 4 July, 2024;
originally announced July 2024.
-
Multiplicity Problems on Algebraic Series and Context-Free Grammars
Authors:
Nikhil Balaji,
Lorenzo Clemente,
Klara Nosan,
Mahsa Shirmohammadi,
James Worrell
Abstract:
In this paper we obtain complexity bounds for computational problems on algebraic power series over several commuting variables. The power series are specified by systems of polynomial equations: a formalism closely related to weighted context-free grammars. We focus on three problems -- decide whether a given algebraic series is identically zero, determine whether all but finitely many coefficien…
▽ More
In this paper we obtain complexity bounds for computational problems on algebraic power series over several commuting variables. The power series are specified by systems of polynomial equations: a formalism closely related to weighted context-free grammars. We focus on three problems -- decide whether a given algebraic series is identically zero, determine whether all but finitely many coefficients are zero, and compute the coefficient of a specific monomial. We relate these questions to well-known computational problems on arithmetic circuits and thereby show that all three problems lie in the counting hierarchy. Our main result improves the best known complexity bound on deciding zeroness of an algebraic series. This problem is known to lie in PSPACE by reduction to the decision problem for the existential fragment of the theory of real closed fields. Here we show that the problem lies in the counting hierarchy by reduction to the problem of computing the degree of a polynomial given by an arithmetic circuit. As a corollary we obtain new complexity bounds on multiplicity equivalence of context-free grammars restricted to a bounded language, language inclusion of a nondeterministic finite automaton in an unambiguous context-free grammar, and language inclusion of a non-deterministic context-free grammar in an unambiguous finite automaton.
△ Less
Submitted 28 April, 2023; v1 submitted 27 April, 2023;
originally announced April 2023.
-
On Rational Recursive Sequences
Authors:
Lorenzo Clemente,
Maria Donten-Bury,
Filip Mazowiecki,
Michał Pilipczuk
Abstract:
We study the class of rational recursive sequences (ratrec) over the rational numbers. A ratrec sequence is defined via a system of sequences using mutually recursive equations of depth 1, where the next values are computed as rational functions of the previous values. An alternative class is that of simple ratrec sequences, where one uses a single recursive equation, however of depth k: the next…
▽ More
We study the class of rational recursive sequences (ratrec) over the rational numbers. A ratrec sequence is defined via a system of sequences using mutually recursive equations of depth 1, where the next values are computed as rational functions of the previous values. An alternative class is that of simple ratrec sequences, where one uses a single recursive equation, however of depth k: the next value is defined as a rational function of k previous values.
We conjecture that the classes ratrec and simple ratrec coincide. The main contribution of this paper is a proof of a variant of this conjecture where the initial conditions are treated symbolically, using a formal variable per sequence, while the sequences themselves consist of rational functions over those variables. While the initial conjecture does not follow from this variant, we hope that the introduced algebraic techniques may eventually be helpful in resolving the problem.
The class ratrec strictly generalises a well-known class of polynomial recursive sequences (polyrec). These are defined like ratrec, but using polynomial functions instead of rational ones. One can observe that if our conjecture is true and effective, then we can improve the complexities of the zeroness and the equivalence problems for polyrec sequences. Currently, the only known upper bound is Ackermanian, which follows from results on polynomial automata. We complement this observation by proving a PSPACE lower bound for both problems for polyrec. Our lower bound construction also implies that the Skolem problem is PSPACE-hard for the polyrec class.
△ Less
Submitted 4 October, 2022;
originally announced October 2022.
-
Using digital traces to build prospective and real-time county-level early warning systems to anticipate COVID-19 outbreaks in the United States
Authors:
Lucas M. Stolerman,
Leonardo Clemente,
Canelle Poirier,
Kris V. Parag,
Atreyee Majumder,
Serge Masyn,
Bernd Resch,
Mauricio Santillana
Abstract:
The ongoing COVID-19 pandemic continues to affect communities around the world. To date, almost 6 million people have died as a consequence of COVID-19, and more than one-quarter of a billion people are estimated to have been infected worldwide. The design of appropriate and timely mitigation strategies to curb the effects of this and future disease outbreaks requires close monitoring of their spa…
▽ More
The ongoing COVID-19 pandemic continues to affect communities around the world. To date, almost 6 million people have died as a consequence of COVID-19, and more than one-quarter of a billion people are estimated to have been infected worldwide. The design of appropriate and timely mitigation strategies to curb the effects of this and future disease outbreaks requires close monitoring of their spatio-temporal trajectories. We present machine learning methods to anticipate sharp increases in COVID-19 activity in US counties in real-time. Our methods leverage Internet-based digital traces -- e.g., disease-related Internet search activity from the general population and clinicians, disease-relevant Twitter micro-blogs, and outbreak trajectories from neighboring locations -- to monitor potential changes in population-level health trends. Motivated by the need for finer spatial-resolution epidemiological insights to improve local decision-making, we build upon previous retrospective research efforts originally conceived at the state level and in the early months of the pandemic. Our methods -- tested in real-time and in an out-of-sample manner on a subset of 97 counties distributed across the US -- frequently anticipated sharp increases in COVID-19 activity 1-6 weeks before the onset of local outbreaks (defined as the time when the effective reproduction number $R_t$ becomes larger than 1 consistently). Given the continued emergence of COVID-19 variants of concern -- such as the most recent one, Omicron -- and the fact that multiple countries have not had full access to vaccines, the framework we present, while conceived for the county-level in the US, could be helpful in countries where similar data sources are available.
△ Less
Submitted 12 March, 2022;
originally announced March 2022.
-
Foothold Evaluation Criterion for Dynamic Transition Feasibility for Quadruped Robots
Authors:
Luca Clemente,
Octavio Villarreal,
Angelo Bratta,
Michele Focchi,
Victor Barasuol,
Giovanni Gerardo Muscolo,
Claudio Semini
Abstract:
To traverse complex scenarios reliably a legged robot needs to move its base aided by the ground reaction forces, which can only be generated by the legs that are momentarily in contact with the ground. A proper selection of footholds is crucial for maintaining balance. In this paper, we propose a foothold evaluation criterion that considers the transition feasibility for both linear and angular d…
▽ More
To traverse complex scenarios reliably a legged robot needs to move its base aided by the ground reaction forces, which can only be generated by the legs that are momentarily in contact with the ground. A proper selection of footholds is crucial for maintaining balance. In this paper, we propose a foothold evaluation criterion that considers the transition feasibility for both linear and angular dynamics to overcome complex scenarios. We devise convex and nonlinear formulations as a direct extension of the Continuous Convex Resolution of Centroidal Dynamic Trajectories (C-CROC) in a receding-horizon fashion to grant dynamic feasibility for future behaviours. The criterion is integrated with a Vision-based Foothold Adaptation (VFA) strategy that takes into account the robot kinematics, leg collisions and terrain morphology. We verify the validity of the selected footholds and the generated trajectories in simulation and experiments with the 90kg quadruped robot HyQ.
△ Less
Submitted 8 March, 2022;
originally announced March 2022.
-
Deterministic and game separability for regular languages of infinite trees
Authors:
Lorenzo Clemente,
Michał Skrzypczak
Abstract:
We show that it is decidable whether two regular languages of infinite trees are separable by a deterministic language, resp., a game language. We consider two variants of separability, depending on whether the set of priorities of the separator is fixed, or not. In each case, we show that separability can be decided in EXPTIME, and that separating automata of exponential size suffice. We obtain o…
▽ More
We show that it is decidable whether two regular languages of infinite trees are separable by a deterministic language, resp., a game language. We consider two variants of separability, depending on whether the set of priorities of the separator is fixed, or not. In each case, we show that separability can be decided in EXPTIME, and that separating automata of exponential size suffice. We obtain our results by reducing to infinite duration games with ω-regular winning conditions and applying the finite-memory determinacy theorem of Büchi and Landweber.
△ Less
Submitted 3 May, 2021;
originally announced May 2021.
-
Determinisability of register and timed automata
Authors:
Lorenzo Clemente,
Sławomir Lasota,
Radosław Piórkowski
Abstract:
The deterministic membership problem for timed automata asks whether the timed language given by a nondeterministic timed automaton can be recognised by a deterministic timed automaton. An analogous problem can be stated in the setting of register automata. We draw the complete decidability/complexity landscape of the deterministic membership problem, in the setting of both register and timed auto…
▽ More
The deterministic membership problem for timed automata asks whether the timed language given by a nondeterministic timed automaton can be recognised by a deterministic timed automaton. An analogous problem can be stated in the setting of register automata. We draw the complete decidability/complexity landscape of the deterministic membership problem, in the setting of both register and timed automata. For register automata, we prove that the deterministic membership problem is decidable when the input automaton is a nondeterministic one-register automaton (possibly with epsilon transitions) and the number of registers of the output deterministic register automaton is fixed. This is optimal: We show that in all the other cases the problem is undecidable, i.e., when either (1) the input nondeterministic automaton has two registers or more (even without epsilon transitions), or (2) it uses guessing, or (3) the number of registers of the output deterministic automaton is not fixed. The landscape for timed automata follows a similar pattern. We show that the problem is decidable when the input automaton is a one-clock nondeterministic timed automaton without epsilon transitions and the number of clocks of the output deterministic timed automaton is fixed. Again, this is optimal: We show that the problem in all the other cases is undecidable, i.e., when either (1) the input nondeterministic timed automaton has two clocks or more, or (2) it uses epsilon transitions, or (3) the number of clocks of the output deterministic automaton is not fixed.
△ Less
Submitted 9 May, 2022; v1 submitted 8 April, 2021;
originally announced April 2021.
-
Bidimensional linear recursive sequences and universality of unambiguous register automata
Authors:
Corentin Barloy,
Lorenzo Clemente
Abstract:
We study the universality and inclusion problems for register automata over equality data. We show that the universality and the inclusion problems can be solved with 2-EXPTIME complexity when the input automata are without guessing and unambiguous, improving on the currently best-known 2-EXPSPACE upper bound by Mottet and Quaas. When the number of registers of both automata is fixed, we obtain a…
▽ More
We study the universality and inclusion problems for register automata over equality data. We show that the universality and the inclusion problems can be solved with 2-EXPTIME complexity when the input automata are without guessing and unambiguous, improving on the currently best-known 2-EXPSPACE upper bound by Mottet and Quaas. When the number of registers of both automata is fixed, we obtain a lower EXPTIME complexity, also improving the EXPSPACE upper bound from Mottet and Quaas for fixed number of registers. We reduce inclusion to universality, and then we reduce universality to the problem of counting the number of orbits of runs of the automaton. We show that the orbit-counting function satisfies a system of bidimensional linear recursive equations with polynomial coefficients (linrec), which generalises analogous recurrences for the Stirling numbers of the second kind, and then we show that universality reduces to the zeroness problem for linrec sequences. While such a counting approach is classical and has successfully been applied to unambiguous finite automata and grammars over finite alphabets, its application to register automata over infinite alphabets is novel. We provide two algorithms to decide the zeroness problem for bidimensional linear recursive sequences arising from orbit-counting functions. Both algorithms rely on techniques from linear non-commutative algebra. The first algorithm performs variable elimination and has elementary complexity. The second algorithm is a refined version of the first one and it relies on the computation of the Hermite normal form of matrices over a skew polynomial field. The second algorithm yields an EXPTIME decision procedure for the zeroness problem of linrec sequences, which in turn yields the claimed bounds for the universality and inclusion problems of register automata.
△ Less
Submitted 4 January, 2021;
originally announced January 2021.
-
Reachability relations of timed pushdown automata
Authors:
Lorenzo Clemente,
Sławomir Lasota
Abstract:
Timed pushdown automata (TPDA) are an expressive formalism combining recursion with a rich logic of timing constraints. We prove that reachability relations of TPDA are expressible in linear arithmetic, a rich logic generalising Presburger arithmetic and rational arithmetic. The main technical ingredients are a novel quantifier elimination result for clock constraints (used to simplify the syntax…
▽ More
Timed pushdown automata (TPDA) are an expressive formalism combining recursion with a rich logic of timing constraints. We prove that reachability relations of TPDA are expressible in linear arithmetic, a rich logic generalising Presburger arithmetic and rational arithmetic. The main technical ingredients are a novel quantifier elimination result for clock constraints (used to simplify the syntax of TPDA transitions), the use of clock difference relations to express reachability relations of the fractional clock values, and an application of Parikh's theorem to reconstruct the integral clock values.
△ Less
Submitted 30 December, 2020;
originally announced December 2020.
-
On the Complexity of the Universality and Inclusion Problems for Unambiguous Context-Free Grammars
Authors:
Lorenzo Clemente
Abstract:
We study the computational complexity of universality and inclusion problems for unambiguous finite automata and context-free grammars. We observe that several such problems can be reduced to the universality problem for unambiguous context-free grammars. The latter problem has long been known to be decidable and we propose a PSPACE algorithm that works by reduction to the zeroness problem of recu…
▽ More
We study the computational complexity of universality and inclusion problems for unambiguous finite automata and context-free grammars. We observe that several such problems can be reduced to the universality problem for unambiguous context-free grammars. The latter problem has long been known to be decidable and we propose a PSPACE algorithm that works by reduction to the zeroness problem of recurrence equations with convolution. We are not aware of any non-trivial complexity lower bounds. However, we show that computing the coin-flip measure of an unambiguous context-free language, a quantitative generalisation of universality, is hard for the long-standing open problem SQRTSUM.
△ Less
Submitted 6 August, 2020;
originally announced August 2020.
-
Determinisability of one-clock timed automata
Authors:
Lorenzo Clemente,
Sławomir Lasota,
Radosław Piórkowski
Abstract:
The deterministic membership problem for timed automata asks whether the timed language recognised by a nondeterministic timed automaton can be recognised by a deterministic timed automaton. We show that the problem is decidable when the input automaton is a one-clock nondeterministic timed automaton without epsilon transitions and the number of clocks of the deterministic timed automaton is fixed…
▽ More
The deterministic membership problem for timed automata asks whether the timed language recognised by a nondeterministic timed automaton can be recognised by a deterministic timed automaton. We show that the problem is decidable when the input automaton is a one-clock nondeterministic timed automaton without epsilon transitions and the number of clocks of the deterministic timed automaton is fixed. We show that the problem in all the other cases is undecidable, i.e., when either 1) the input nondeterministic timed automaton has two clocks or more, or 2) it uses epsilon transitions, or 3) the number of clocks of the output deterministic automaton is not fixed.
△ Less
Submitted 18 July, 2020;
originally announced July 2020.
-
An Early Warning Approach to Monitor COVID-19 Activity with Multiple Digital Traces in Near Real-Time
Authors:
Nicole E. Kogan,
Leonardo Clemente,
Parker Liautaud,
Justin Kaashoek,
Nicholas B. Link,
Andre T. Nguyen,
Fred S. Lu,
Peter Huybers,
Bernd Resch,
Clemens Havas,
Andreas Petutschnig,
Jessica Davis,
Matteo Chinazzi,
Backtosch Mustafa,
William P. Hanage,
Alessandro Vespignani,
Mauricio Santillana
Abstract:
Non-pharmaceutical interventions (NPIs) have been crucial in curbing COVID-19 in the United States (US). Consequently, relaxing NPIs through a phased re-opening of the US amid still-high levels of COVID-19 susceptibility could lead to new epidemic waves. This calls for a COVID-19 early warning system. Here we evaluate multiple digital data streams as early warning indicators of increasing or decre…
▽ More
Non-pharmaceutical interventions (NPIs) have been crucial in curbing COVID-19 in the United States (US). Consequently, relaxing NPIs through a phased re-opening of the US amid still-high levels of COVID-19 susceptibility could lead to new epidemic waves. This calls for a COVID-19 early warning system. Here we evaluate multiple digital data streams as early warning indicators of increasing or decreasing state-level US COVID-19 activity between January and June 2020. We estimate the timing of sharp changes in each data stream using a simple Bayesian model that calculates in near real-time the probability of exponential growth or decay. Analysis of COVID-19-related activity on social network microblogs, Internet searches, point-of-care medical software, and a metapopulation mechanistic model, as well as fever anomalies captured by smart thermometer networks, shows exponential growth roughly 2-3 weeks prior to comparable growth in confirmed COVID-19 cases and 3-4 weeks prior to comparable growth in COVID-19 deaths across the US over the last 6 months. We further observe exponential decay in confirmed cases and deaths 5-6 weeks after implementation of NPIs, as measured by anonymized and aggregated human mobility data from mobile phones. Finally, we propose a combined indicator for exponential growth in multiple data streams that may aid in develo** an early warning system for future COVID-19 outbreaks. These efforts represent an initial exploratory framework, and both continued study of the predictive power of digital indicators as well as further development of the statistical approach are needed.
△ Less
Submitted 3 July, 2020; v1 submitted 1 July, 2020;
originally announced July 2020.
-
On the complexity of the universality and inclusion problems for unambiguous context-free grammars (technical report)
Authors:
Lorenzo Clemente
Abstract:
We study the computational complexity of universality and inclusion problems for unambiguous finite automata and context-free grammars. We observe that several such problems can be reduced to the universality problem for unambiguous context-free grammars. The latter problem has long been known to be decidable and we propose a PSPACE algorithm that works by reduction to the zeroness problem of recu…
▽ More
We study the computational complexity of universality and inclusion problems for unambiguous finite automata and context-free grammars. We observe that several such problems can be reduced to the universality problem for unambiguous context-free grammars. The latter problem has long been known to be decidable and we propose a PSPACE algorithm that works by reduction to the zeroness problem of recurrence equations with convolution. We are not aware of any non-trivial complexity lower bounds. However, we show that computing the coin-flip measure of an unambiguous context-free language, a quantitative generalisation of universality, is hard for the long-standing open problem SQRTSUM.
△ Less
Submitted 11 June, 2020; v1 submitted 9 June, 2020;
originally announced June 2020.
-
Timed games and deterministic separability
Authors:
Lorenzo Clemente,
Sławomir Lasota,
Radosław Piórkowski
Abstract:
We study a generalisation of Büchi-Landweber games to the timed setting. The winning condition is specified by a non-deterministic timed automaton with epsilon transitions and only Player I can elapse time. We show that for fixed number of clocks and maximal numerical constant available to Player II, it is decidable whether she has a winning timed controller using these resources. More interesting…
▽ More
We study a generalisation of Büchi-Landweber games to the timed setting. The winning condition is specified by a non-deterministic timed automaton with epsilon transitions and only Player I can elapse time. We show that for fixed number of clocks and maximal numerical constant available to Player II, it is decidable whether she has a winning timed controller using these resources. More interestingly, we also show that the problem remains decidable even when the maximal numerical constant is not specified in advance, which is an important technical novelty not present in previous literature on timed games. We complement these two decidability result by showing undecidability when the number of clocks available to Player II is not fixed. As an application of timed games, and our main motivation to study them, we show that they can be used to solve the deterministic separability problem for nondeterministic timed automata with epsilon transitions. This is a novel decision problem about timed automata which has not been studied before. We show that separability is decidable when the number of clocks of the separating automaton is fixed and the maximal constant is not. The problem whether separability is decidable without bounding the number of clocks of the separator remains an interesting open problem.
△ Less
Submitted 27 April, 2020;
originally announced April 2020.
-
Cost Automata, Safe Schemes, and Downward Closures
Authors:
David Barozzini,
Lorenzo Clemente,
Thomas Colcombet,
Paweł Parys
Abstract:
In this work we prove decidability of the model-checking problem for safe recursion schemes against properties defined by alternating B-automata. We then exploit this result to show how to compute downward closures of languages of finite trees recognized by safe recursion schemes.
Higher-order recursion schemes are an expressive formalism used to define languages of finite and infinite ranked tr…
▽ More
In this work we prove decidability of the model-checking problem for safe recursion schemes against properties defined by alternating B-automata. We then exploit this result to show how to compute downward closures of languages of finite trees recognized by safe recursion schemes.
Higher-order recursion schemes are an expressive formalism used to define languages of finite and infinite ranked trees by means of fixed points of lambda terms. They extend regular and context-free grammars, and are equivalent in expressive power to the simply typed $λY$-calculus and collapsible pushdown automata. Safety in a syntactic restriction which limits their expressive power.
The class of alternating B-automata is an extension of alternating parity automata over infinite trees; it enhances them with counting features that can be used to describe boundedness properties.
△ Less
Submitted 28 March, 2023; v1 submitted 25 April, 2020;
originally announced April 2020.
-
A machine learning methodology for real-time forecasting of the 2019-2020 COVID-19 outbreak using Internet searches, news alerts, and estimates from mechanistic models
Authors:
Dianbo Liu,
Leonardo Clemente,
Canelle Poirier,
Xiyu Ding,
Matteo Chinazzi,
Jessica T Davis,
Alessandro Vespignani,
Mauricio Santillana
Abstract:
We present a timely and novel methodology that combines disease estimates from mechanistic models with digital traces, via interpretable machine-learning methodologies, to reliably forecast COVID-19 activity in Chinese provinces in real-time. Specifically, our method is able to produce stable and accurate forecasts 2 days ahead of current time, and uses as inputs (a) official health reports from C…
▽ More
We present a timely and novel methodology that combines disease estimates from mechanistic models with digital traces, via interpretable machine-learning methodologies, to reliably forecast COVID-19 activity in Chinese provinces in real-time. Specifically, our method is able to produce stable and accurate forecasts 2 days ahead of current time, and uses as inputs (a) official health reports from Chinese Center Disease for Control and Prevention (China CDC), (b) COVID-19-related internet search activity from Baidu, (c) news media activity reported by Media Cloud, and (d) daily forecasts of COVID-19 activity from GLEAM, an agent-based mechanistic model. Our machine-learning methodology uses a clustering technique that enables the exploitation of geo-spatial synchronicities of COVID-19 activity across Chinese provinces, and a data augmentation technique to deal with the small number of historical disease activity observations, characteristic of emerging outbreaks. Our model's predictive power outperforms a collection of baseline models in 27 out of the 32 Chinese provinces, and could be easily extended to other geographies currently affected by the COVID-19 outbreak to help decision makers.
△ Less
Submitted 8 April, 2020;
originally announced April 2020.
-
Timed Basic Parallel Processes
Authors:
Lorenzo Clemente,
Piotr Hofman,
Patrick Totzke
Abstract:
Timed basic parallel processes (TBPP) extend communication-free Petri nets (aka. BPP or commutative context-free grammars) by a global notion of time. TBPP can be seen as an extension of timed automata (TA) with context-free branching rules, and as such may be used to model networks of independent timed automata with process creation.
We show that the coverability and reachability problems (with…
▽ More
Timed basic parallel processes (TBPP) extend communication-free Petri nets (aka. BPP or commutative context-free grammars) by a global notion of time. TBPP can be seen as an extension of timed automata (TA) with context-free branching rules, and as such may be used to model networks of independent timed automata with process creation.
We show that the coverability and reachability problems (with unary encoded target multiplicities) are PSPACE-complete and EXPTIME-complete, respectively. For the special case of 1-clock TBPP, both are NP-complete and hence not more complex than for untimed BPP. This contrasts with known super-Ackermannian-completeness and undecidability results for general timed Petri nets.
As a result of independent interest, and basis for our NP upper bounds, we show that the reachability relation of 1-clock TA can be expressed by a formula of polynomial size in the existential fragment of linear arithmetic, which improves on recent results from the literature.
△ Less
Submitted 8 July, 2019; v1 submitted 2 July, 2019;
originally announced July 2019.
-
Binary reachability of timed pushdown automata via quantifier elimination and cyclic order atoms
Authors:
Lorenzo Clemente,
Sławomir Lasota
Abstract:
We study an expressive model of timed pushdown automata extended with modular and fractional clock constraints. We show that the binary reachability relation is effectively expressible in hybrid linear arithmetic with a rational and an integer sort. This subsumes analogous expressibility results previously known for finite and pushdown timed automata with untimed stack. As key technical tools, we…
▽ More
We study an expressive model of timed pushdown automata extended with modular and fractional clock constraints. We show that the binary reachability relation is effectively expressible in hybrid linear arithmetic with a rational and an integer sort. This subsumes analogous expressibility results previously known for finite and pushdown timed automata with untimed stack. As key technical tools, we use quantifier elimination for a fragment of hybrid linear arithmetic and for cyclic order atoms, and a reduction to register pushdown automata over cyclic order atoms.
△ Less
Submitted 28 April, 2018;
originally announced April 2018.
-
Decidability of Timed Communicating Automata
Authors:
Lorenzo Clemente
Abstract:
We study the reachability problem for networks of timed communicating processes. Each process is a timed automaton communicating with other processes by exchanging messages over unbounded FIFO channels. Messages carry clocks which are checked at the time of transmission and reception with suitable timing constraints. Each automaton can only access its set of local clocks and message clocks of sent…
▽ More
We study the reachability problem for networks of timed communicating processes. Each process is a timed automaton communicating with other processes by exchanging messages over unbounded FIFO channels. Messages carry clocks which are checked at the time of transmission and reception with suitable timing constraints. Each automaton can only access its set of local clocks and message clocks of sent/received messages. Time is dense and all clocks evolve at the same rate. Our main contribution is a complete characterisation of decidable and undecidable communication topologies generalising and unifying previous work. From a technical point of view, we use quantifier elimination and a reduction to counter automata with registers.
△ Less
Submitted 20 April, 2018;
originally announced April 2018.
-
Efficient reduction of nondeterministic automata with application to language inclusion testing
Authors:
Lorenzo Clemente,
Richard Mayr
Abstract:
We present efficient algorithms to reduce the size of nondeterministic Büchi word automata (NBA) and nondeterministic finite word automata (NFA), while retaining their languages. Additionally, we describe methods to solve PSPACE-complete automata problems like language universality, equivalence, and inclusion for much larger instances than was previously possible ($\ge 1000$ states instead of 10-1…
▽ More
We present efficient algorithms to reduce the size of nondeterministic Büchi word automata (NBA) and nondeterministic finite word automata (NFA), while retaining their languages. Additionally, we describe methods to solve PSPACE-complete automata problems like language universality, equivalence, and inclusion for much larger instances than was previously possible ($\ge 1000$ states instead of 10-100). This can be used to scale up applications of automata in formal verification tools and decision procedures for logical theories. The algorithms are based on new techniques for removing transitions (pruning) and adding transitions (saturation), as well as extensions of classic quotienting of the state space. These techniques use criteria based on combinations of backward and forward trace inclusions and simulation relations. Since trace inclusion relations are themselves PSPACE-complete, we introduce lookahead simulations as good polynomial time computable approximations thereof. Extensive experiments show that the average-case time complexity of our algorithms scales slightly above quadratically. (The space complexity is worst-case quadratic.) The size reduction of the automata depends very much on the class of instances, but our algorithm consistently reduces the size far more than all previous techniques. We tested our algorithms on NBA derived from LTL-formulae, NBA derived from mutual exclusion protocols and many classes of random NBA and NFA, and compared their performance to the well-known automata tool GOAL.
△ Less
Submitted 12 February, 2019; v1 submitted 27 November, 2017;
originally announced November 2017.
-
Regular Separability of Parikh Automata
Authors:
Lorenzo Clemente,
Wojciech Czerwiński,
Sławomir Lasota,
Charles Paperman
Abstract:
We investigate a subclass of languages recognized by vector addition systems, namely languages of nondeterministic Parikh automata. While the regularity problem (is the language of a given automaton regular?) is undecidable for this model, we show surprising decidability of the regular separability problem: given two Parikh automata, is there a regular language that contains one of them and is dis…
▽ More
We investigate a subclass of languages recognized by vector addition systems, namely languages of nondeterministic Parikh automata. While the regularity problem (is the language of a given automaton regular?) is undecidable for this model, we show surprising decidability of the regular separability problem: given two Parikh automata, is there a regular language that contains one of them and is disjoint from the other?
△ Less
Submitted 19 December, 2016;
originally announced December 2016.
-
Separability of Reachability Sets of Vector Addition Systems
Authors:
Lorenzo Clemente,
Wojciech Czerwiński,
Sławomir Lasota,
Charles Paperman
Abstract:
Given two families of sets $\mathcal{F}$ and $\mathcal{G}$, the $\mathcal{F}$ separability problem for $\mathcal{G}$ asks whether for two given sets $U, V \in \mathcal{G}$ there exists a set $S \in \mathcal{F}$, such that $U$ is included in $S$ and $V$ is disjoint with $S$. We consider two families of sets $\mathcal{F}$: modular sets $S \subseteq \mathbb{N}^d$, defined as unions of equivalence cla…
▽ More
Given two families of sets $\mathcal{F}$ and $\mathcal{G}$, the $\mathcal{F}$ separability problem for $\mathcal{G}$ asks whether for two given sets $U, V \in \mathcal{G}$ there exists a set $S \in \mathcal{F}$, such that $U$ is included in $S$ and $V$ is disjoint with $S$. We consider two families of sets $\mathcal{F}$: modular sets $S \subseteq \mathbb{N}^d$, defined as unions of equivalence classes modulo some natural number $n \in \mathbb{N}$, and unary sets. Our main result is decidability of modular and unary separability for the class $\mathcal{G}$ of reachability sets of Vector Addition Systems, Petri Nets, Vector Addition Systems with States, and for sections thereof.
△ Less
Submitted 1 September, 2016;
originally announced September 2016.
-
The Diagonal Problem for Higher-Order Recursion Schemes is Decidable
Authors:
Lorenzo Clemente,
Paweł Parys,
Sylvain Salvati,
Igor Walukiewicz
Abstract:
A non-deterministic recursion scheme recognizes a language of finite trees. This very expressive model can simulate, among others, higher-order pushdown automata with collapse. We show decidability of the diagonal problem for schemes. This result has several interesting consequences. In particular, it gives an algorithm that computes the downward closure of languages of words recognized by schemes…
▽ More
A non-deterministic recursion scheme recognizes a language of finite trees. This very expressive model can simulate, among others, higher-order pushdown automata with collapse. We show decidability of the diagonal problem for schemes. This result has several interesting consequences. In particular, it gives an algorithm that computes the downward closure of languages of words recognized by schemes. In turn, this has immediate application to separability problems and reachability analysis of concurrent systems.
△ Less
Submitted 2 May, 2016;
originally announced May 2016.
-
Non-Zero Sum Games for Reactive Synthesis
Authors:
Romain Brenguier,
Lorenzo Clemente,
Paul Hunter,
Guillermo A. Pérez,
Mickael Randour,
Jean-François Raskin,
Ocan Sankur,
Mathieu Sassolas
Abstract:
In this invited contribution, we summarize new solution concepts useful for the synthesis of reactive systems that we have introduced in several recent publications. These solution concepts are developed in the context of non-zero sum games played on graphs. They are part of the contributions obtained in the inVEST project funded by the European Research Council.
In this invited contribution, we summarize new solution concepts useful for the synthesis of reactive systems that we have introduced in several recent publications. These solution concepts are developed in the context of non-zero sum games played on graphs. They are part of the contributions obtained in the inVEST project funded by the European Research Council.
△ Less
Submitted 17 December, 2015;
originally announced December 2015.
-
Ordered Tree-Pushdown Systems
Authors:
Lorenzo Clemente,
Paweł Parys,
Sylvain Salvati,
Igor Walukiewicz
Abstract:
We define a new class of pushdown systems where the pushdown is a tree instead of a word. We allow a limited form of lookahead on the pushdown conforming to a certain ordering restriction, and we show that the resulting class enjoys a decidable reachability problem. This follows from a preservation of recognizability result for the backward reachability relation of such systems. As an application,…
▽ More
We define a new class of pushdown systems where the pushdown is a tree instead of a word. We allow a limited form of lookahead on the pushdown conforming to a certain ordering restriction, and we show that the resulting class enjoys a decidable reachability problem. This follows from a preservation of recognizability result for the backward reachability relation of such systems. As an application, we show that our simple model can encode several formalisms generalizing pushdown systems, such as ordered multi-pushdown systems, annotated higher-order pushdown systems, the Krivine machine, and ordered annotated multi-pushdown systems. In each case, our procedure yields tight complexity.
△ Less
Submitted 12 October, 2015;
originally announced October 2015.
-
No Fine theorem for macrorealism: Limitations of the Leggett-Garg inequality
Authors:
Lucas Clemente,
Johannes Kofler
Abstract:
Tests of local realism and macrorealism have historically been discussed in very similar terms: Leggett-Garg inequalities follow Bell inequalities as necessary conditions for classical behavior. Here, we compare the probability polytopes spanned by all measurable probability distributions for both scenarios and show that their structure differs strongly between spatially and temporally separated m…
▽ More
Tests of local realism and macrorealism have historically been discussed in very similar terms: Leggett-Garg inequalities follow Bell inequalities as necessary conditions for classical behavior. Here, we compare the probability polytopes spanned by all measurable probability distributions for both scenarios and show that their structure differs strongly between spatially and temporally separated measurements. We arrive at the conclusion that, in contrast to tests of local realism where Bell inequalities form a necessary and sufficient set of conditions, no set of inequalities can ever be necessary and sufficient for a macrorealistic description. Fine's famous proof that Bell inequalities are necessary and sufficient for the existence of a local realistic model, therefore cannot be transferred to macrorealism. A recently proposed condition, no-signaling in time, fulfills this criterion, and we show why it is better suited for future experimental tests and theoretical studies of macrorealism. Our work thereby identifies a major difference between the mathematical structures of local realism and macrorealism.
△ Less
Submitted 21 April, 2016; v1 submitted 1 September, 2015;
originally announced September 2015.
-
Multidimensional beyond worst-case and almost-sure problems for mean-payoff objectives
Authors:
Lorenzo Clemente,
Jean-François Raskin
Abstract:
The beyond worst-case threshold problem (BWC), recently introduced by Bruyère et al., asks given a quantitative game graph for the synthesis of a strategy that i) enforces some minimal level of performance against any adversary, and ii) achieves a good expectation against a stochastic model of the adversary. They solved the BWC problem for finite-memory strategies and unidimensional mean-payoff ob…
▽ More
The beyond worst-case threshold problem (BWC), recently introduced by Bruyère et al., asks given a quantitative game graph for the synthesis of a strategy that i) enforces some minimal level of performance against any adversary, and ii) achieves a good expectation against a stochastic model of the adversary. They solved the BWC problem for finite-memory strategies and unidimensional mean-payoff objectives and they showed membership of the problem in NP$\cap$coNP. They also noted that infinite-memory strategies are more powerful than finite-memory ones, but the respective threshold problem was left open. We extend these results in several directions. First, we consider multidimensional mean-payoff objectives. Second, we study both finite-memory and infinite-memory strategies. We show that the multidimensional BWC problem is coNP-complete in both cases. Third, in the special case when the worst-case objective is unidimensional (but the expectation objective is still multidimensional) we show that the complexity decreases to NP$\cap$coNP. This solves the infinite-memory threshold problem left open by Bruyère et al., and this complexity cannot be improved without improving the currently known complexity of classical mean-payoff games. Finally, we introduce a natural relaxation of the BWC problem, the beyond almost-sure threshold problem (BAS), which asks for the synthesis of a strategy that ensures some minimal level of performance with probability one and a good expectation against the stochastic model of the adversary. We show that the multidimensional BAS threshold problem is solvable in P.
△ Less
Submitted 21 November, 2017; v1 submitted 30 April, 2015;
originally announced April 2015.
-
Reachability analysis of first-order definable pushdown systems
Authors:
Lorenzo Clemente,
Sławomir Lasota
Abstract:
We study pushdown systems where control states, stack alphabet, and transition relation, instead of being finite, are first-order definable in a fixed countably-infinite structure. We show that the reachability analysis can be addressed with the well-known saturation technique for the wide class of oligomorphic structures. Moreover, for the more restrictive homogeneous structures, we are able to g…
▽ More
We study pushdown systems where control states, stack alphabet, and transition relation, instead of being finite, are first-order definable in a fixed countably-infinite structure. We show that the reachability analysis can be addressed with the well-known saturation technique for the wide class of oligomorphic structures. Moreover, for the more restrictive homogeneous structures, we are able to give concrete complexity upper bounds. We show ample applicability of our technique by presenting several concrete examples of homogeneous structures, subsuming, with optimal complexity, known results from the literature. We show that infinitely many such examples of homogeneous structures can be obtained with the classical wreath product construction.
△ Less
Submitted 17 July, 2015; v1 submitted 10 April, 2015;
originally announced April 2015.
-
Timed pushdown automata revisited
Authors:
Lorenzo Clemente,
Sławomir Lasota
Abstract:
This paper contains two results on timed extensions of pushdown automata (PDA). As our first result we prove that the model of dense-timed PDA of Abdulla et al. collapses: it is expressively equivalent to dense-timed PDA with timeless stack. Motivated by this result, we advocate the framework of first-order definable PDA, a specialization of PDA in sets with atoms, as the right setting to define a…
▽ More
This paper contains two results on timed extensions of pushdown automata (PDA). As our first result we prove that the model of dense-timed PDA of Abdulla et al. collapses: it is expressively equivalent to dense-timed PDA with timeless stack. Motivated by this result, we advocate the framework of first-order definable PDA, a specialization of PDA in sets with atoms, as the right setting to define and investigate timed extensions of PDA. The general model obtained in this way is Turing complete. As our second result we prove NEXPTIME upper complexity bound for the non-emptiness problem for an expressive subclass. As a byproduct, we obtain a tight EXPTIME complexity bound for a more restrictive subclass of PDA with timeless stack, thus subsuming the complexity bound known for dense-timed PDA.
△ Less
Submitted 17 April, 2015; v1 submitted 9 March, 2015;
originally announced March 2015.
-
Necessary and sufficient conditions for macroscopic realism from quantum mechanics
Authors:
Lucas Clemente,
Johannes Kofler
Abstract:
Macroscopic realism, the classical world view that macroscopic objects exist independently of and are not influenced by measurements, is usually tested using Leggett-Garg inequalities. Recently, another necessary condition called no-signaling in time (NSIT) has been proposed as a witness for non-classical behavior. In this paper, we show that a combination of NSIT conditions is not only necessary…
▽ More
Macroscopic realism, the classical world view that macroscopic objects exist independently of and are not influenced by measurements, is usually tested using Leggett-Garg inequalities. Recently, another necessary condition called no-signaling in time (NSIT) has been proposed as a witness for non-classical behavior. In this paper, we show that a combination of NSIT conditions is not only necessary but also sufficient for a macrorealistic description of a physical system. Any violation of macroscopic realism must therefore be witnessed by a suitable NSIT condition. Subsequently, we derive an operational formulation for NSIT in terms of positive operator-valued measurements and the system Hamiltonian. We argue that this leads to a suitable definition of "classical" measurements and Hamiltonians, and apply our formalism to some generic coarse-grained quantum measurements.
△ Less
Submitted 8 June, 2015; v1 submitted 29 January, 2015;
originally announced January 2015.
-
Stochastic Parity Games on Lossy Channel Systems
Authors:
Parosh Aziz Abdulla,
Lorenzo Clemente,
Richard Mayr,
Sven Sandberg
Abstract:
We give an algorithm for solving stochastic parity games with almost-sure winning conditions on {\it lossy channel systems}, under the constraint that both players are restricted to finite-memory strategies. First, we describe a general framework, where we consider the class of 2 1/2-player games with almost-sure parity winning conditions on possibly infinite game graphs, assuming that the game co…
▽ More
We give an algorithm for solving stochastic parity games with almost-sure winning conditions on {\it lossy channel systems}, under the constraint that both players are restricted to finite-memory strategies. First, we describe a general framework, where we consider the class of 2 1/2-player games with almost-sure parity winning conditions on possibly infinite game graphs, assuming that the game contains a {\it finite attractor}. An attractor is a set of states (not necessarily absorbing) that is almost surely re-visited regardless of the players' decisions. We present a scheme that characterizes the set of winning states for each player. Then, we instantiate this scheme to obtain an algorithm for {\it stochastic game lossy channel systems}.
△ Less
Submitted 1 January, 2015; v1 submitted 15 October, 2014;
originally announced October 2014.
-
Unified Analysis of Collapsible and Ordered Pushdown Automata via Term Rewriting
Authors:
Lorenzo Clemente
Abstract:
We model collapsible and ordered pushdown systems with term rewriting, by encoding higher-order stacks and multiple stacks into trees. We show a uniform inverse preservation of recognizability result for the resulting class of term rewriting systems, which is obtained by extending the classic saturation-based approach. This result subsumes and unifies similar analyses on collapsible and ordered pu…
▽ More
We model collapsible and ordered pushdown systems with term rewriting, by encoding higher-order stacks and multiple stacks into trees. We show a uniform inverse preservation of recognizability result for the resulting class of term rewriting systems, which is obtained by extending the classic saturation-based approach. This result subsumes and unifies similar analyses on collapsible and ordered pushdown systems. Despite the rich literature on inverse preservation of recognizability for term rewrite systems, our result does not seem to follow from any previous study.
△ Less
Submitted 15 October, 2014;
originally announced October 2014.
-
Proceedings 15th International Workshop on Verification of Infinite-State Systems
Authors:
Lukas Holik,
Lorenzo Clemente
Abstract:
This volume contains the proceedings of Infinity'13, the 15th International Workshop on Verification of Infinite-State Systems, which was held in Hanoi, Vietnam on the 14th of October 2013 as a satellite event of ATVA'13. The aim of the INFINITY workshop is to provide a forum for researchers interested in the development of formal methods and algorithmic techniques for the analysis of systems with…
▽ More
This volume contains the proceedings of Infinity'13, the 15th International Workshop on Verification of Infinite-State Systems, which was held in Hanoi, Vietnam on the 14th of October 2013 as a satellite event of ATVA'13. The aim of the INFINITY workshop is to provide a forum for researchers interested in the development of formal methods and algorithmic techniques for the analysis of systems with infinitely many states, and their application in automated verification of complex software and hardware systems.
△ Less
Submitted 23 February, 2014;
originally announced February 2014.
-
Stochastic Parity Games on Lossy Channel Systems
Authors:
Parosh Aziz Abdulla,
Lorenzo Clemente,
Richard Mayr,
Sven Sandberg
Abstract:
We give an algorithm for solving stochastic parity games with almost-sure winning conditions on lossy channel systems, for the case where the players are restricted to finite-memory strategies. First, we describe a general framework, where we consider the class of 2.5-player games with almost-sure parity winning conditions on possibly infinite game graphs, assuming that the game contains a finite…
▽ More
We give an algorithm for solving stochastic parity games with almost-sure winning conditions on lossy channel systems, for the case where the players are restricted to finite-memory strategies. First, we describe a general framework, where we consider the class of 2.5-player games with almost-sure parity winning conditions on possibly infinite game graphs, assuming that the game contains a finite attractor. An attractor is a set of states (not necessarily absorbing) that is almost surely re-visited regardless of the players' decisions. We present a scheme that characterizes the set of winning states for each player. Then, we instantiate this scheme to obtain an algorithm for stochastic game lossy channel systems.
△ Less
Submitted 13 June, 2013; v1 submitted 22 May, 2013;
originally announced May 2013.
-
Advanced Automata Minimization
Authors:
Lorenzo Clemente,
Richard Mayr
Abstract:
We present an efficient algorithm to reduce the size of nondeterministic Buchi word automata, while retaining their language. Additionally, we describe methods to solve PSPACE-complete automata problems like universality, equivalence and inclusion for much larger instances (1-3 orders of magnitude) than before. This can be used to scale up applications of automata in formal verification tools and…
▽ More
We present an efficient algorithm to reduce the size of nondeterministic Buchi word automata, while retaining their language. Additionally, we describe methods to solve PSPACE-complete automata problems like universality, equivalence and inclusion for much larger instances (1-3 orders of magnitude) than before. This can be used to scale up applications of automata in formal verification tools and decision procedures for logical theories. The algorithm is based on new transition pruning techniques. These use criteria based on combinations of backward and forward trace inclusions. Since these relations are themselves PSPACE-complete, we describe methods to compute good approximations of them in polynomial time. Extensive experiments show that the average-case complexity of our algorithm scales quadratically. The size reduction of the automata depends very much on the class of instances, but our algorithm consistently outperforms all previous techniques by a wide margin. We tested our algorithm on Buchi automata derived from LTL-formulae, many classes of random automata and automata derived from mutual exclusion protocols, and compared its performance to the well-known automata tool GOAL.
△ Less
Submitted 24 October, 2012;
originally announced October 2012.
-
Reachability of Communicating Timed Processes
Authors:
Lorenzo Clemente,
Frédéric Herbreteau,
Amélie Stainer,
Grégoire Sutre
Abstract:
We study the reachability problem for communicating timed processes, both in discrete and dense time. Our model comprises automata with local timing constraints communicating over unbounded FIFO channels. Each automaton can only access its set of local clocks; all clocks evolve at the same rate. Our main contribution is a complete characterization of decidable and undecidable communication topolog…
▽ More
We study the reachability problem for communicating timed processes, both in discrete and dense time. Our model comprises automata with local timing constraints communicating over unbounded FIFO channels. Each automaton can only access its set of local clocks; all clocks evolve at the same rate. Our main contribution is a complete characterization of decidable and undecidable communication topologies, for both discrete and dense time. We also obtain complexity results, by showing that communicating timed processes are at least as hard as Petri nets; in the discrete time, we also show equivalence with Petri nets. Our results follow from mutual topology-preserving reductions between timed automata and (untimed) counter automata.
△ Less
Submitted 17 October, 2012; v1 submitted 4 September, 2012;
originally announced September 2012.
-
Quantum Magnetomechanics with Levitating Superconducting Microspheres
Authors:
O. Romero-Isart,
L. Clemente,
C. Navau,
A. Sanchez,
J. I. Cirac
Abstract:
We show that by magnetically trap** a superconducting microsphere close to a quantum circuit, it is experimentally feasible to perform ground-state cooling and to prepare quantum superpositions of the center-of-mass motion of the microsphere. Due to the absence of clam** losses and time dependent electromagnetic fields, the mechanical motion of micrometer-sized metallic spheres in the Meissner…
▽ More
We show that by magnetically trap** a superconducting microsphere close to a quantum circuit, it is experimentally feasible to perform ground-state cooling and to prepare quantum superpositions of the center-of-mass motion of the microsphere. Due to the absence of clam** losses and time dependent electromagnetic fields, the mechanical motion of micrometer-sized metallic spheres in the Meissner state is predicted to be very well isolated from the environment. Hence, we propose to combine the technology of magnetic microtraps and superconducting qubits to bring relatively large objects to the quantum regime.
△ Less
Submitted 7 March, 2012; v1 submitted 23 December, 2011;
originally announced December 2011.
-
Büchi Automata can have Smaller Quotients
Authors:
Lorenzo Clemente
Abstract:
We study novel simulation-like preorders for quotienting nondeterministic Büchi automata. We define fixed-word delayed simulation, a new preorder coarser than delayed simulation. We argue that fixed-word simulation is the coarsest forward simulation-like preorder which can be used for quotienting Büchi automata, thus improving our understanding of the limits of quotienting. Also, we show that comp…
▽ More
We study novel simulation-like preorders for quotienting nondeterministic Büchi automata. We define fixed-word delayed simulation, a new preorder coarser than delayed simulation. We argue that fixed-word simulation is the coarsest forward simulation-like preorder which can be used for quotienting Büchi automata, thus improving our understanding of the limits of quotienting. Also, we show that computing fixed-word simulation is PSPACE-complete. On the practical side, we introduce proxy simulations, which are novel polynomial-time computable preorders sound for quotienting. In particular, delayed proxy simulation induce quotients that can be smaller by an arbitrarily large factor than direct backward simulation. We derive proxy simulations as the product of a theory of refinement transformers: A refinement transformer maps preorders non-decreasingly, preserving certain properties. We study under which general conditions refinement transformers are sound for quotienting.
△ Less
Submitted 26 April, 2011; v1 submitted 16 February, 2011;
originally announced February 2011.
-
Quantum memories based on engineered dissipation
Authors:
Fernando Pastawski,
Lucas Clemente,
Juan Ignacio Cirac
Abstract:
Storing quantum information for long times without disruptions is a major requirement for most quantum information technologies. A very appealing approach is to use self-correcting Hamiltonians, i.e. tailoring local interactions among the qubits such that when the system is weakly coupled to a cold bath the thermalization process takes a long time. Here we propose an alternative but more powerful…
▽ More
Storing quantum information for long times without disruptions is a major requirement for most quantum information technologies. A very appealing approach is to use self-correcting Hamiltonians, i.e. tailoring local interactions among the qubits such that when the system is weakly coupled to a cold bath the thermalization process takes a long time. Here we propose an alternative but more powerful approach in which the coupling to a bath is engineered, so that dissipation protects the encoded qubit against more general kinds of errors. We show that the method can be implemented locally in four dimensional lattice geometries by means of a toric code, and propose a simple 2D set-up for proof of principle experiments.
△ Less
Submitted 31 January, 2011; v1 submitted 14 October, 2010;
originally announced October 2010.
