~~NOCACHE~~ /* DO NOT EDIT THIS FILE */ [[en:seminaires:verif:index|Verification]]\\ Monday December 13, 2021, 11AM, [[https://u-paris.zoom.us/j/87413678251?pwd=Wmg5cTNuSy9XMnFNdlJhRFkrR3F5dz09|Zoom link]]\\ **Angelo Ferrando** (University of Genova) //Towards Runtime Verification of ROS applications// \\ In this talk I am going to introduce Runtime Verification and its use in the context of robotic applications developed in ROS (Robot Operating System). Specifically, I will present a recent framework, called ROSMonitoring, which has been recently developed to verify message exchange in ROS. All the engineering steps will be presented, as well as some interesting robotic case study where ROSMonitoring has been applied. [[en:seminaires:verif:index|Verification]]\\ Monday December 6, 2021, 11AM, 1007 and [[https://u-paris.zoom.us/j/87413678251?pwd=Wmg5cTNuSy9XMnFNdlJhRFkrR3F5dz09|Zoom link]]\\ **Alessio Mansutti** (University of Oxford) //Efficient complementation of semilinear sets and the VC dimension of Presburger arithmetic// \\ We discuss the issue of deciding the first-order theory of integer linear arithmetic, also known as Presburger arithmetic. Whereas optimal decision procedures based on either quantifier-elimination or automata constructions are known for this theory, the current procedures based on manipulating semilinear sets (i.e. sets that geometrically characterise the solutions of a formula) are extremely inefficient. We address this issue by deriving a new algorithm for computing the complement of a semilinear set, which in particular is optimal for nested complementations. Alongside solving the aforementioned discrepancy between semilinear-based algorithms and other types of procedures, this result allows us to characterise the Vapnik-Chervonenkis dimension of Presburger arithmetic, which is found to be doubly-exponential. The results in this talk are joint work with Christoph Haase and Dmitry Chistikov. [[en:seminaires:verif:index|Verification]]\\ Monday November 22, 2021, 11AM, 3058 and [[https://u-paris.zoom.us/j/87413678251?pwd=Wmg5cTNuSy9XMnFNdlJhRFkrR3F5dz09|Zoom link]]\\ **Patricia Bouyer-Decitre** (FML - CNRS) //On the (Approximate) Analysis of Stochastic Real-Time Systems// \\ Analyzing stochastic systems with real-time features is notably difficult, and often calls for approximation technics. In this talk I will present a crucial property of stochastic systems, which allows for provably sound approximated model-checking technics. This property, called decisiveness, was first proposed by Abdulla et al in 2007 for infinite-state discrete Markov chains. This was later extended to general stochastic transition systems, and general approximation schemes were proven correct for large classes of properties. Finally it turns out that several classes of real-time stochastic systems that have been considered in the literature do actually satisfy the property, which implies that they can safely be analysed. This talk is based on joint works with Nathalie Bertrand, Thomas Brihaye, Pierre Carlier, Mickael Randour, Cedric Riviere and Pierre Vandenhove. This talk is proposed in the context of the ANR project MAVeriQ day. [[en:seminaires:verif:index|Verification]]\\ Monday October 18, 2021, 11AM, 3052 and [[https://u-paris.zoom.us/j/87413678251?pwd=Wmg5cTNuSy9XMnFNdlJhRFkrR3F5dz09|Zoom link]]\\ **Florian Renkin** (LRDE, EPITA) //Practical "Paritizing" of Emerson-Lei Automata// \\ We introduce a new algorithm that takes a Transition-based Emerson-Lei Automaton (TELA), that is, an ω-automaton whose acceptance condition is an arbitrary Boolean formula on sets of transitions to be seen infinitely or finitely often, and converts it into a Transition-based Parity Automaton (TPA). To reduce the size of the output TPA, the algorithm combines and optimizes two procedures based on a latest appearance record principle, and introduces a partial degeneralization. Our motivation is to use this algorithm to improve our LTL synthesis tool, where producing deterministic parity automata is an intermediate step. Séminaire qui peut aussi intéresser l'équipe Automates [[en:seminaires:verif:index|Verification]]\\ Monday September 27, 2021, 11AM, 1007 and [[https://u-paris.zoom.us/j/87413678251?pwd=Wmg5cTNuSy9XMnFNdlJhRFkrR3F5dz09|Zoom link]]\\ **Paula Herber** (University of Münster) //Contract-based Verification of Hybrid Simulink Models with Differential Dynamic Logic// \\ Cyber-physical systems, where digital components interact with a physical environment, are ubiquitous in our everyday lives. Digital devices assist our households, monitor our health, and support our transportation in airplanes, trains, or cars. While the complexity of cyber-physical systems is steadily increasing, a failure in such systems can have serious consequences. Model-driven development provides an approach to cope with the increasing complexity, but has the serious drawback that industrially used modeling languages, such as Matlab/Simulink, have only informally defined semantics. To overcome this problem, we propose to precisely capture the semantics of hybrid Simulink models with an automated transformation into the formally well-defined differential dynamic logic (dL). Our transformation enables us to formally verify crucial safety properties of hybrid Simulink models with the interactive theorem prover KeYmaera X. KeYmaera X enables deductive reasoning and thus has the potential to scale well even for larger systems. However, the interactive verification with KeYmaera X is still expensive in terms of manual effort and required expertise. To reduce the verification effort, we propose to define /hybrid contracts/, which enable compositional verification, but still have to be defined manually. In this talk, I will summarize our transformation from Simulink to dL, hybrid contracts for compositional verification, and then discuss the idea of using /hybrid contract patterns/ to ease the interactive verification of cyber-physical systems with KeYmaera X. [[en:seminaires:verif:index|Verification]]\\ Monday September 13, 2021, 11AM, 3052 and [[https://bbb-front.math.univ-paris-diderot.fr/recherche/ber-rxi-tol-i7y|BBB link]]\\ **Lukáš Holík** (Brno University of Technology) //Regex matching with counting-set automata// \\ We propose a solution to the problem of efficient matching regular expressions (regexes) with bounded repetition, such as (ab){1,100}, using deterministic automata. For this, we introduce novel /counting-set automata (CsAs)/, automata with registers that can hold sets of bounded integers and can be manipulated by a limited portfolio of constant-time operations. We present an algorithm that compiles a large sub-class of regexes to deterministic CsAs. This includes (1) a novel Antimirov-style translation of regexes with counting to /counting automata (CAs)/, nondeterministic automata with bounded counters, and (2) our main technical contribution, a determinization of CAs that outputs CsAs. The main advantage of this workflow is that /the size of the produced CsAs does not depend on the repetition bounds used in the regex/ (while the size of the DFA is exponential to them). Our experimental results confirm that deterministic CsAs produced from practical regexes with repetition are indeed vastly smaller than the corresponding DFAs. More importantly, our prototype matcher based on CsA simulation handles practical regexes with repetition regardless of sizes of counter bounds. It easily copes with regexes with repetition where state-of-the-art matchers struggle. [[en:seminaires:verif:index|Verification]]\\ Monday July 5, 2021, 11AM, 3052 and [[https://bbb-front.math.univ-paris-diderot.fr/recherche/ber-rxi-tol-i7y|BBB link]]\\ **Eugène Asarin** (IRIF, Université de Paris) //On the complexity of timed pattern matching// \\ (joint work with Thomas Ferrère, Dejan Nickovic and Dogan Ulus) Timed pattern matching consists in finding occurrences of a timed regular expression in a timed word. This problem has been addressed using several techniques, its solutions are implemented in tools (quite efficient in practice), and used, for example in log analysis and runtime verification. In this work, we explore computational complexity of timed pattern matching, and prove P, NP and PSPACE bounds, depending on connectives used in expressions and other details. We conclude with a couple of open questions. [[en:seminaires:verif:index|Verification]]\\ Monday June 28, 2021, 11AM, [[https://bbb-front.math.univ-paris-diderot.fr/recherche/ber-rxi-tol-i7y|BBB link]]\\ **Emmanuel Filiot** (Université Libre de Bruxelles) //On Some Transducer Synthesis Problems// \\ The seminal Büchi-Landweber theorem states that reactive synthesis from omega-automatic specifications is decidable, or equivalently, the synthesis problem from specifications given by non-deterministic synchronous (aka letter-to-letter) transducers. Moreover, when such a specification is realizable, it is realizable by a deterministic synchronous transducer. In this talk, we consider variants and generalizations of this problem, on finite and infinite words, where the synchronicity assumption is relaxed on the specification side and/or the implementation side. [[en:seminaires:verif:index|Verification]]\\ Monday June 14, 2021, 11AM, 3052 and [[https://bbb-front.math.univ-paris-diderot.fr/recherche/ber-rxi-tol-i7y|BBB link]]\\ **Arnaud Sangnier** (IRIF, Université de Paris) //Reachability in Distributed Memory Automata// \\ We introduce Distributed Memory Automata, a model of register automata suitable to capture some features of distributed algorithms designed for shared memory systems. In this model, each participant owns a local register and a shared register and has the ability to change its local value, to write it in the global memory and to test atomically the number of occurrences of its value in the shared memory, up to some threshold. We show that the control state reachability problem for Distributed Memory Automata is Pspace-complete for a fixed number of participants and is in Pspace when the number of participants is not fixed a priori. This is a joint work with Benedikt Bollig and Fedor Ryabinin. We try an hybrid session. Dependending on technicalities, the visioconference platform may change. [[en:seminaires:verif:index|Verification]]\\ Monday June 7, 2021, 11AM, [[https://bbb-front.math.univ-paris-diderot.fr/recherche/ber-rxi-tol-i7y|BBB link]]\\ **Bernadette Charron-Bost** (LIX, École Polytechnique) //Foundational Aspects of the Blockchain Consensus// \\ Decentralized cryptocurrencies such as Bitcoin have ignited much excitement, not only for their novel realization of central bank-free financial instruments, but also as an alternative approach for the development of numerous distributed applications in which agreement must be reached without central control and despite misbehaving parties. The soundness and security of these applications, however, hinge on the thorough understanding of the fundamental properties of their underlying blockchain data structure that parties (“miners”) maintain and try to extend by generating “proofs of work”. In this talk we formulate such fundamental properties of the blockchain ---"common prefix", "chain quality", "chain growth"--- and show how the blockchain consensus differs from the classical problem of consensus in distributed computing and from the consensus in control theory. We analyze the impact of different setups, computational assumptions, and network models on the various properties of the blockchain consensus. We also examine the crucial role of the “proofs of work” for achieving network synchrony on top of unstructured P2P networks. [[en:seminaires:verif:index|Verification]]\\ Monday May 17, 2021, 11AM, [[https://bbb-front.math.univ-paris-diderot.fr/recherche/ber-rxi-tol-i7y|BBB link]]\\ **Sidi Mohamed Beillahi** (IRIF) //Checking Robustness Between Weak Transactional Consistency Models// \\ Concurrent accesses to databases are typically encapsulated in transactions in order to enable isolation from other concurrent computations and resilience to failures. Modern databases provide transactions with various semantics corresponding to different trade-offs between consistency and availability. Since a weaker consistency model provides better performance, an important issue is investigating the weakest level of consistency needed by a given program (to satisfy its specification). As a way of dealing with this issue, we investigate the problem of checking whether a given program has the same set of behaviors when replacing a consistency model with a weaker one. This property known as robustness generally implies that any specification of the program is preserved when weakening the consistency. We focus on the robustness problem for consistency models which are weaker than standard serializability, namely, causal consistency, prefix consistency, and snapshot isolation. We show that checking robustness between these models is polynomial time reducible to a state reachability problem under serializability. We use this reduction to also derive a pragmatic proof technique based on Lipton's reduction theory that allows to prove programs robust. We have applied our techniques to several challenging applications drawn from the literature of distributed systems and databases. This a joint work with Ahmed Bouajjani and Constantin Enea. [[en:seminaires:verif:index|Verification]]\\ Monday May 10, 2021, 11AM, [[https://bbb-front.math.univ-paris-diderot.fr/recherche/ber-rxi-tol-i7y|BBB link]]\\ **Laurent Doyen** (LMF — ENS Saclay) //Observation and Distinction. Representing Information in Infinite Games// \\ We compare two approaches for modelling imperfect information in infinite games by using finite-state automata. The first, more standard approach views information as the result of an observation process driven by a sequential Mealy machine. In contrast, the second approach features indistinguishability relations described by synchronous two-tape automata. The indistinguishability-relation model turns out to be strictly more expressive than the one based on observations. We present a characterisation of the indistinguishability relations that admit a representation as a finite-state observation function. We show that the characterisation is decidable, and give a procedure to construct a corresponding Mealy machine whenever one exists. The talk is based on joint work with Dietmar Berwanger. [[en:seminaires:verif:index|Verification]]\\ Monday April 12, 2021, 11AM, [[https://bbb-front.math.univ-paris-diderot.fr/recherche/ber-rxi-tol-i7y|BBB link]]\\ **Jérôme Leroux** (LABRI) //Flat Petri nets// \\ Vector addition systems with states (VASS), or equivalently vector addition systems, or Petri nets are a long established model of concurrency with extensive applications. The central algorithmic problem is reachability: whether from a given initial configuration there exists a sequence of valid execution steps that reaches a 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 computation. In this presentation, we survey results about the reachability problem focusing on flat VASS. This subclass is central for computing the reachability set of general VASS using Presburger arithmetic. In fact, the reachability set of a VASS is Presburger if, and only if, it is flattable, i.e. the computation of its reachability set is reducible to the computation of the reachability set of a flat VASS. Whereas the reachability problem for flat VASS is clearly NP-complete in any fix dimension when numbers are encoded in binary, finding the exact complexity of the reachability problem for flat VASS in unary is a difficult (still open) problem. [[en:seminaires:verif:index|Verification]]\\ Monday March 22, 2021, 11AM, [[https://bbb-front.math.univ-paris-diderot.fr/recherche/ber-rxi-tol-i7y|BBB link]]\\ **James Worrell** (University of Oxford) //Dynamical Systems and Program Analysis// \\ This talk is about the algorithmic analysis of dynamical systems and its relevance to the foundations of program analysis. A dynamical system is a state-based system that is specified by a rule specifying how the state changes over time (e.g., a swinging pendulum or a cobweb model of supply and demand in economics). While the study of dynamical systems permeates the quantitative sciences, in this talk we focus on computational aspects and their relevance to basic verification problems, such as termination and invariant synthesis. We highlight in particular certain problems that can be traced back to the program-analysis literature, e.g., concerning the decidability of termination for linear constraint loops and the computability of polyhedral and polynomial invariants for various classes of transition systems. In the talk we give some of the mathematical context of these problems, discuss recent progress, and highlight unsolved cases. The characteristic feature of the problems we consider is that they turn out to be much more challenging than they might first appear to the innocent-minded and in some cases have connections to problems at the frontiers of modern mathematics. [[en:seminaires:verif:index|Verification]]\\ Monday March 15, 2021, 11AM, [[https://bbb-front.math.univ-paris-diderot.fr/recherche/ber-rxi-tol-i7y|BBB link]]\\ **Stefan Kiefer** (University of Oxford) //How to play in infinite MDPs// \\ Markov decision processes (MDPs) are a standard model for dynamic systems that exhibit both stochastic and nondeterministic behavior. For MDPs with finite state space it is known that for a wide range of objectives there exist optimal strategies that are memoryless and deterministic. In contrast, if the state space is infinite, the picture is much richer: optimal strategies may not exist, and optimal or epsilon-optimal strategies may require (possibly infinite) memory. Based on many examples, I am going to give an introduction to a collection of techniques that allow for the construction of strategies with little or no memory in countably infinite MDPs. Video available here https://www.youtube.com/watch?v=OFXkmtbgPUo [[en:seminaires:verif:index|Verification]]\\ Monday March 1, 2021, 11AM, [[https://bbb-front.math.univ-paris-diderot.fr/recherche/ber-rxi-tol-i7y|BBB link]]\\ **Mahsa Shirmohammadi** (IRIF, CNRS) //Cyclotomic Identity Testing and Applications// \\ We consider the cyclotomic identity testing (CIT) problem: given a polynomial~$f(x_1,\ldots,x_k)$, decide whether $f(\zeta_n^{e_1},\ldots,\zeta_n^{e_k})$ is zero, where $\zeta_n = e^{2\pi i/n}$ is a primitive complex $n$-th root of unity and $e_1,\ldots,e_k$ are integers, represented in binary. When~$f$ is given by an algebraic circuit, we give a randomized polynomial-time algorithm for CIT assuming the generalised Riemann hypothesis (GRH), and show that the problem is in coNP unconditionally. When $f$ is given by a circuit of polynomially bounded degree, we give a randomized NC algorithm. In case $f$ is a linear form we show that the problem lies in NC. Towards understanding when CIT can be solved in deterministic polynomial-time, we consider so-called diagonal depth-3 circuits, i.e., polynomials $f=\sum_{i=1}^m g_i^{d_i}$, where $g_i$ is a linear form and $d_i$ a positive integer given in unary. We observe that a polynomial-time algorithm for CIT on this class would yield a sub-exponential-time algorithm for polynomial identity testing. However, assuming GRH, we show that if the linear forms~$g_i$ are all identical then CIT can be solved in polynomial time. Finally, we use our results to give a new proof that equality of compressed strings, i.e., strings presented using context-free grammars, can be decided in randomized NC. [[en:seminaires:verif:index|Verification]]\\ Thursday February 25, 2021, 4PM, [[https://bbb-front.math.univ-paris-diderot.fr/recherche/ber-rxi-tol-i7y|BBB link]]\\ **Shaz Qadeer** (Novi Research, Seattle) //Reifying Concurrent Programs// \\ Program reification is a new approach to the construction of verified concurrent programs and their proofs. This approach simplifies and scales (human and automated) reasoning by enabling a concurrent program to be represented and manipulated at multiple layers of abstraction. These abstraction layers are chained together via simple program transformations; each transformation is justified by a collection of automatically checked verification conditions. Program reification makes proofs maintainable and reusable, specifically eliminating the need to write complex invariants on the low-level encoding of the concurrent program as a flat transition system. I will present Civl, a reifier for concurrent programs. Civl has been used to construct verified low-level implementations of complex systems such as a concurrent garbage collector, consensus protocol, and shared-memory data structures. Civl is publicly available: https://civl-verifier.github.io/ . This work has been done jointly with Bernhard Kragl (IST Austria). [[en:seminaires:verif:index|Verification]]\\ Monday February 22, 2021, 11AM, [[https://bbb-front.math.univ-paris-diderot.fr/recherche/ber-rxi-tol-i7y|BBB link]]\\ **Mohammed Foughali** (Vérimag, Université Grenoble-Alpes) //On the formal verification of safety-critical systems: challenges, approaches and perspectives// \\ Safety-critical applications, e.g. those stemming from robotic, autonomous and cyber-physical systems, must be formally verified against crucial behavioral and timed properties. Yet, the use of formal verification techniques in such context faces a number of challenges, such as the absence of formal foundations of robotic frameworks and the lack of scalability of exhaustive verification techniques. In this talk, I will explore the approaches I have been proposing for the last six years to tackle these challenges, based on a global vision that favors correctness, user-friendliness and scalability of formal methods vis-à-vis real-world robotic and autonomous systems deployed on embedded platforms. I will discuss a major part of my work where safety-critical specifications are automatically translated into strictly equivalent formal models on which model checking, but also scalable non exhaustive techniques such as statistical model checking and runtime verification, may be used by practitioners to gain a considerable amount of trust in their underlying applications. Further, I will present a couple of techniques that allow to take into account hardware and OS specificities in the verification process, such as the scheduling policy and the number of processor cores provided by the platform, and thus increase the meaningfulness of the verification results. I will conclude with possible future research directions within the broad objective of deploying trustable safety-critical systems through bridging the gap between the software engineering, robotics, formal methods and real-time systems communities. [[en:seminaires:verif:index|Verification]]\\ Monday February 15, 2021, 11AM, [[https://bbb-front.math.univ-paris-diderot.fr/recherche/ber-rxi-tol-i7y|BBB link]]\\ **Martin Helfrich** (Technical University of Munich) //Succinct Population Protocols for Presburger Arithmetic// \\ In [Dana Angluin et al., 2006], Angluin et al. proved that population protocols compute exactly the predicates definable in Presburger arithmetic (PA), the first-order theory of addition. As part of this result, they presented a procedure that translates any formula φ of quantifier-free PA with remainder predicates (which has the same expressive power as full PA) into a population protocol with 2^????(poly(|φ|)) states that computes φ. More precisely, the number of states of the protocol is exponential in both the bit length of the largest coefficient in the formula, and the number of nodes of its syntax tree. In this paper, we prove that every formula φ of quantifier-free PA with remainder predicates is computable by a leaderless population protocol with ????(poly(|φ|)) states. Our proof is based on several new constructions, which may be of independent interest. Given a formula φ of quantifier-free PA with remainder predicates, a first construction produces a succinct protocol (with ????(|φ|³) leaders) that computes φ; this completes the work initiated in [Michael Blondin et al., 2018], where we constructed such protocols for a fragment of PA. For large enough inputs, we can get rid of these leaders. If the input is not large enough, then it is small, and we design another construction producing a succinct protocol with one leader that computes φ. Our last construction gets rid of this leader for small inputs. [[en:seminaires:verif:index|Verification]]\\ Monday February 8, 2021, 11AM, [[https://bbb-front.math.univ-paris-diderot.fr/recherche/ber-rxi-tol-i7y|BBB link]]\\ **Blaise Genest** (IRISA (CNRS)) //Global PAC Bounds for Learning Discrete Time Markov Chains.// \\ Learning models from observations of a system is a powerful tool with many applications. In this paper, we consider learning Discrete Time Markov Chains (DTMC), with different methods such as frequency estimation or Laplace smoothing. While models learnt with such methods converge asymptotically towards the exact system, a more practical question in the realm of trusted machine learning is how accurate a model learnt with a limited time budget is. Existing approaches provide bounds on how close the model is to the original system, in terms of bounds on local (transition) probabilities, which has unclear implication on the global behavior. In this work, we provide global bounds on the error made by such a learning process, in terms of global behaviors formalized using temporal logic. More precisely, we propose a learning process ensuring a bound on the error in the probabilities of these properties. While such learning process cannot exist for the full LTL logic, we provide one ensuring a bound that is uniform over all the formulas of CTL. Further, given one time-to-failure property, we provide an improved learning algorithm. Interestingly, frequency estimation is sufficient for the latter, while Laplace smoothing is needed to ensure non-trivial uniform bounds for the full CTL logic. [[en:seminaires:verif:index|Verification]]\\ Monday February 1, 2021, 11AM, [[https://bbb-front.math.univ-paris-diderot.fr/recherche/ber-rxi-tol-i7y|BBB link]]\\ **François Schwarzentruber** (IRISA, ENS Rennes) //Connected multi-agent path finding// \\ Motivated by the increasing appeal of robots in information-gathering missions, we study multi-agent path planning problems in which the agents must remain interconnected. We model an area by a topological graph specifying the movement and the connectivity constraints of the agents. In the first part of the talk, we study the theoretical complexity of the reachability and the coverage problems of a fleet of connected agents. We also introduce a new class called sight-moveable graphs which admit efficient algorithms. In the second part, we re-visit the conflict-based search algorithm known for multi-agent path finding, and define a variant where conflicts arise from disconnections rather than collisions. [[en:seminaires:verif:index|Verification]]\\ Monday January 18, 2021, 11AM, [[https://bbb-front.math.univ-paris-diderot.fr/recherche/ber-rxi-tol-i7y|BBB link]]\\ **Léo Henry** (IRISA, Université de Rennes I) //Active learning of timed automata with unobservable resets// \\ Active learning of timed languages is concerned with the inference of timed automata from observed timed words. The agent can query for the membership of words in the target language, or propose a candidate model and verify its equivalence to the target. The major difficulty of this framework is the inference of clock resets, central to the dynamics of timed automata, but not directly observable. Interesting first steps have already been made by restricting to the subclass of event-recording automata, where clock resets are tied to observations. In order to advance towards learning of general timed automata, we generalize this method to a new class, called reset-free event-recording automata, where some transitions may reset no clocks. This offers the same challenges as generic timed automata while keeping the simpler framework of event-recording automata for the sake of readability. Central to our contribution is the notion of invalidity, and the algorithm and data structures to deal with it, allowing on-the-fly detection and pruning of reset hypotheses that contradict observations, a key to any efficient active-learning procedure for generic timed automata. [[en:seminaires:verif:index|Verification]]\\ Monday January 11, 2021, 11AM, [[https://bbb-front.math.univ-paris-diderot.fr/recherche/ber-rxi-tol-i7y|BBB link]]\\ **Mohamed Faouzi Atig** (Uppsala University) //Parameterized verification under TSO is PSPACE-complete.// \\ We consider parameterized verification of concurrent programs under the Total Store Order (TSO) semantics. A program consists of a set of processes that share a set of variables on which they can perform read and write operations. We show that the reachability problem for a system consisting of an arbitrary number of identical processes is PSPACE-complete. We prove that the complexity is reduced to polynomial time if the processes are not allowed to read the initial values of the variables in the memory. When the processes are allowed to perform atomic read-modify-write operations, the reachability problem has a non-primitive recursive complexity.