Showing 1–19 of 19 results for author: Dimitrova, R

Localized Attractor Computations for Infinite-State Games (Full Version)

Authors: Anne-Kathrin Schmuck, Philippe Heim, Rayna Dimitrova, Satya Prakash Nayak

Abstract: Infinite-state games are a commonly used model for the synthesis of reactive systems with unbounded data domains. Symbolic methods for solving such games need to be able to construct intricate arguments to establish the existence of winning strategies. Often, large problem instances require prohibitively complex arguments. Therefore, techniques that identify smaller and simpler sub-problems and ex… ▽ More Infinite-state games are a commonly used model for the synthesis of reactive systems with unbounded data domains. Symbolic methods for solving such games need to be able to construct intricate arguments to establish the existence of winning strategies. Often, large problem instances require prohibitively complex arguments. Therefore, techniques that identify smaller and simpler sub-problems and exploit the respective results for the given game-solving task are highly desirable. In this paper, we propose the first such technique for infinite-state games. The main idea is to enhance symbolic game-solving with the results of localized attractor computations performed in sub-games. The crux of our approach lies in identifying useful sub-games by computing permissive winning strategy templates in finite abstractions of the infinite-state game. The experimental evaluation of our method demonstrates that it outperforms existing techniques and is applicable to infinite-state games beyond the state of the art. △ Less

Submitted 15 May, 2024; originally announced May 2024.

Comments: This is a full version of paper accepted at CAV 2024

Solving Infinite-State Games via Acceleration (Full Version)

Authors: Philippe Heim, Rayna Dimitrova

Abstract: Two-player graph games have found numerous applications, most notably in the synthesis of reactive systems from temporal specifications, but also in verification. The relevance of infinite-state systems in these areas has lead to significant attention towards develo** techniques for solving infinite-state games. We propose novel symbolic semi-algorithms for solving infinite-state games with te… ▽ More Two-player graph games have found numerous applications, most notably in the synthesis of reactive systems from temporal specifications, but also in verification. The relevance of infinite-state systems in these areas has lead to significant attention towards develo** techniques for solving infinite-state games. We propose novel symbolic semi-algorithms for solving infinite-state games with temporal winning conditions. The novelty of our approach lies in the introduction of an acceleration technique that enhances fixpoint-based game-solving methods and helps to avoid divergence. Classical fixpoint-based algorithms, when applied to infinite-state games, are bound to diverge in many cases, since they iteratively compute the set of states from which one player has a winning strategy. Our proposed approach can lead to convergence in cases where existing algorithms require an infinite number of iterations. This is achieved by acceleration: computing an infinite set of states from which a simpler sub-strategy can be iterated an unbounded number of times in order to win the game. Ours is the first method for solving infinite-state games to employ acceleration. Thanks to this, it is able to outperform state-of-the-art techniques on a range of benchmarks, as evidenced by our evaluation of a prototype implementation. △ Less

Submitted 7 November, 2023; v1 submitted 25 May, 2023; originally announced May 2023.

Comments: This is a full version of paper accepted at POPL 2024

Taming Large Bounds in Synthesis from Bounded-Liveness Specifications (Full Version)

Authors: Philippe Heim, Rayna Dimitrova

Abstract: Automatic synthesis from temporal logic specifications is an attractive alternative to manual system design, due to its ability to generate correct-by-construction implementations from high-level specifications. Due to the high complexity of the synthesis problem, significant research efforts have been directed at develo** practically efficient approaches for restricted specification language fr… ▽ More Automatic synthesis from temporal logic specifications is an attractive alternative to manual system design, due to its ability to generate correct-by-construction implementations from high-level specifications. Due to the high complexity of the synthesis problem, significant research efforts have been directed at develo** practically efficient approaches for restricted specification language fragments. In this paper, we focus on the Safety LTL fragment of Linear Temporal Logic (LTL) syntactically extended with bounded temporal operators. We propose a new synthesis approach with the primary motivation to solve efficiently the synthesis problem for specifications with bounded temporal operators, in particular those with large bounds. The experimental evaluation of our method shows that for this type of specifications, it outperforms state-of-art synthesis tools, demonstrating that it is a promising approach to efficiently treating quantitative timing constraints in safety specifications. △ Less

Submitted 24 January, 2023; originally announced January 2023.

Comments: Full version of paper accepted at TACAS 2023

Synthesizing Approximate Implementations for Unrealizable Specifications

Authors: Rayna Dimitrova, Bernd Finkbeiner, Hazem Torfah

Abstract: The unrealizability of a specification is often due to the assumption that the behavior of the environment is unrestricted. In this paper, we present algorithms for synthesis in bounded environments, where the environment can only generate input sequences that are ultimately periodic words (lassos) with finite representations of bounded size. We provide automata-theoretic and symbolic approaches f… ▽ More The unrealizability of a specification is often due to the assumption that the behavior of the environment is unrestricted. In this paper, we present algorithms for synthesis in bounded environments, where the environment can only generate input sequences that are ultimately periodic words (lassos) with finite representations of bounded size. We provide automata-theoretic and symbolic approaches for solving this synthesis problem, and also study the synthesis of approximative implementations from unrealizable specifications. Such implementations may violate the specification in general, but are guaranteed to satisfy the specification on at least a specified portion of the bounded-size lassos. We evaluate the algorithms on different arbiter specifications. △ Less

Submitted 28 December, 2020; originally announced December 2020.

Comments: Published at CAV 2019

Approximate Automata for Omega-Regular Languages

Authors: Rayna Dimitrova, Bernd Finkbeiner, Hazem Torfah

Abstract: Automata over infinite words, also known as omega-automata, play a key role in the verification and synthesis of reactive systems. The spectrum of omega-automata is defined by two characteristics: the acceptance condition (e.g. Büchi or parity) and the determinism (e.g., deterministic or nondeterministic) of an automaton. These characteristics play a crucial role in applications of automata theory… ▽ More Automata over infinite words, also known as omega-automata, play a key role in the verification and synthesis of reactive systems. The spectrum of omega-automata is defined by two characteristics: the acceptance condition (e.g. Büchi or parity) and the determinism (e.g., deterministic or nondeterministic) of an automaton. These characteristics play a crucial role in applications of automata theory. For example, certain acceptance conditions can be handled more efficiently than others by dedicated tools and algorithms. Furthermore, some applications, such as synthesis and probabilistic model checking, require that properties are represented as some type of deterministic omega-automata. However, properties cannot always be represented by automata with the desired acceptance condition and determinism. In this paper we study the problem of approximating linear-time properties by automata in a given class. Our approximation is based on preserving the language up to a user-defined precision given in terms of the size of the finite lasso representation of infinite executions that are preserved. We study the state complexity of different types of approximating automata, and provide constructions for the approximation within different automata classes, for example, for approximating a given automaton by one with a simpler acceptance condition. △ Less

Submitted 28 December, 2020; originally announced December 2020.

Comments: Published at ATVA 2020

Conformance Relations and Hyperproperties for Do** Detection in Time and Space

Authors: Sebastian Biewer, Rayna Dimitrova, Michael Fries, Maciej Gazda, Thomas Heinze, Holger Hermanns, Mohammad Reza Mousavi

Abstract: We present a novel and generalised notion of do** cleanness for cyber-physical systems that allows for perturbing the inputs and observing the perturbed outputs both in the time- and value-domains. We instantiate our definition using existing notions of conformance for cyber-physical systems. As a formal basis for monitoring conformance-based cleanness, we develop the temporal logic HyperSTL*, a… ▽ More We present a novel and generalised notion of do** cleanness for cyber-physical systems that allows for perturbing the inputs and observing the perturbed outputs both in the time- and value-domains. We instantiate our definition using existing notions of conformance for cyber-physical systems. As a formal basis for monitoring conformance-based cleanness, we develop the temporal logic HyperSTL*, an extension of Signal Temporal Logics with trace quantifiers and a freeze operator. We show that our generalised definitions are essential in a data-driven method for do** detection and apply our definitions to a case study concerning diesel emission tests. △ Less

Submitted 17 January, 2022; v1 submitted 7 December, 2020; originally announced December 2020.

Journal ref: Logical Methods in Computer Science, Volume 18, Issue 1 (January 19, 2022) lmcs:6963

Near-Optimal Reactive Synthesis Incorporating Runtime Information

Authors: Suda Bharadwaj, Abraham P. Vinod, Rayna Dimitrova, Ufuk Topcu

Abstract: We consider the problem of optimal reactive synthesis - compute a strategy that satisfies a mission specification in a dynamic environment, and optimizes a performance metric. We incorporate task-critical information, that is only available at runtime, into the strategy synthesis in order to improve performance. Existing approaches to utilising such time-varying information require online re-synth… ▽ More We consider the problem of optimal reactive synthesis - compute a strategy that satisfies a mission specification in a dynamic environment, and optimizes a performance metric. We incorporate task-critical information, that is only available at runtime, into the strategy synthesis in order to improve performance. Existing approaches to utilising such time-varying information require online re-synthesis, which is not computationally feasible in real-time applications. In this paper, we pre-synthesize a set of strategies corresponding to candidate instantiations (pre-specified representative information scenarios). We then propose a novel switching mechanism to dynamically switch between the strategies at runtime while guaranteeing all safety and liveness goals are met. We also characterize bounds on the performance suboptimality. We demonstrate our approach on two examples - robotic motion planning where the likelihood of the position of the robot's goal is updated in real-time, and an air traffic management problem for urban air mobility. △ Less

Submitted 31 July, 2020; originally announced July 2020.

Comments: Presented at ICRA2020

Probabilistic Hyperproperties of Markov Decision Processes

Authors: Rayna Dimitrova, Bernd Finkbeiner, Hazem Torfah

Abstract: Hyperproperties are properties that describe the correctness of a system as a relation between multiple executions. Hyperproperties generalize trace properties and include information-flow security requirements, like noninterference, as well as requirements like symmetry, partial observation, robustness, and fault tolerance. We initiate the study of the specification and verification of hyperprope… ▽ More Hyperproperties are properties that describe the correctness of a system as a relation between multiple executions. Hyperproperties generalize trace properties and include information-flow security requirements, like noninterference, as well as requirements like symmetry, partial observation, robustness, and fault tolerance. We initiate the study of the specification and verification of hyperproperties of Markov decision processes (MDPs). We introduce the temporal logic PHL (Probabilistic Hyper Logic), which extends classic probabilistic logics with quantification over schedulers and traces. PHL can express a wide range of hyperproperties for probabilistic systems, including both classical applications, such as probabilistic noninterference, and novel applications in areas such as robotics and planning. While the model checking problem for PHL is in general undecidable, we provide methods both for proving and for refuting formulas from a fragment of the logic. The fragment includes many probabilistic hyperproperties of interest. △ Less

Submitted 13 October, 2020; v1 submitted 7 May, 2020; originally announced May 2020.

Comments: Extended version of paper published at ATVA'20

Towards Low-Latency High-Bandwidth Control of Quadrotors using Event Cameras

Authors: Rika Sugimoto Dimitrova, Mathias Gehrig, Dario Brescianini, Davide Scaramuzza

Abstract: Event cameras are a promising candidate to enable high speed vision-based control due to their low sensor latency and high temporal resolution. However, purely event-based feedback has yet to be used in the control of drones. In this work, a first step towards implementing low-latency high-bandwidth control of quadrotors using event cameras is taken. In particular, this paper addresses the problem… ▽ More Event cameras are a promising candidate to enable high speed vision-based control due to their low sensor latency and high temporal resolution. However, purely event-based feedback has yet to be used in the control of drones. In this work, a first step towards implementing low-latency high-bandwidth control of quadrotors using event cameras is taken. In particular, this paper addresses the problem of one-dimensional attitude tracking using a dualcopter platform equipped with an event camera. The event-based state estimation consists of a modified Hough transform algorithm combined with a Kalman filter that outputs the roll angle and angular velocity of the dualcopter relative to a horizon marked by a black-and-white disk. The estimated state is processed by a proportional-derivative attitude control law that computes the rotor thrusts required to track the desired attitude. The proposed attitude tracking scheme shows promising results of event-camera-driven closed loop control: the state estimator performs with an update rate of 1 kHz and a latency determined to be 12 ms, enabling attitude tracking at speeds of over 1600 deg/s. △ Less

Submitted 28 March, 2020; v1 submitted 11 November, 2019; originally announced November 2019.

Journal ref: IEEE International Conference on Robotics and Automation (ICRA), Paris, 2020

Reactive Synthesis with Maximum Realizability of Linear Temporal Logic Specifications

Authors: Rayna Dimitrova, Mahsa Ghasemi, Ufuk Topcu

Abstract: A challenging problem for autonomous systems is to synthesize a reactive controller that conforms to a set of given correctness properties. Linear temporal logic (LTL) provides a formal language to specify the desired behavioral properties of systems. In applications in which the specifications originate from various aspects of the system design, or consist of a large set of formulas, the overall… ▽ More A challenging problem for autonomous systems is to synthesize a reactive controller that conforms to a set of given correctness properties. Linear temporal logic (LTL) provides a formal language to specify the desired behavioral properties of systems. In applications in which the specifications originate from various aspects of the system design, or consist of a large set of formulas, the overall system specification may be unrealizable. Driven by this fact, we develop an optimization variant of synthesis from LTL formulas, where the goal is to design a controller that satisfies a set of hard specifications and minimally violates a set of soft specifications. To that end, we introduce a value function that, by exploiting the LTL semantics, quantifies the level of violation of properties. Inspired by the idea of bounded synthesis, we fix a bound on the implementation size and search for an implementation that is optimal with respect to the said value function. We propose a novel maximum satisfiability encoding of the search for an optimal implementation (within the given bound on the implementation size). We iteratively increase the bound on the implementation size until a termination criterion, such as a threshold over the value function, is met. △ Less

Submitted 4 October, 2019; originally announced October 2019.

Comments: arXiv admin note: substantial text overlap with arXiv:1804.00415

Distributed Synthesis of Surveillance Strategies for Mobile Sensors

Authors: Suda Bharadwaj, Rayna Dimitrova, Ufuk Topcu

Abstract: We study the problem of synthesizing strategies for a mobile sensor network to conduct surveillance in partnership with static alarm triggers. We formulate the problem as a multi-agent reactive synthesis problem with surveillance objectives specified as temporal logic formulas. In order to avoid the state space blow-up arising from a centralized strategy computation, we propose a method to decentr… ▽ More We study the problem of synthesizing strategies for a mobile sensor network to conduct surveillance in partnership with static alarm triggers. We formulate the problem as a multi-agent reactive synthesis problem with surveillance objectives specified as temporal logic formulas. In order to avoid the state space blow-up arising from a centralized strategy computation, we propose a method to decentralize the surveillance strategy synthesis by decomposing the multi-agent game into subgames that can be solved independently. We also decompose the global surveillance specification into local specifications for each sensor, and show that if the sensors satisfy their local surveillance specifications, then the sensor network as a whole will satisfy the global surveillance objective. Thus, our method is able to guarantee global surveillance properties in a mobile sensor network while synthesizing completely decentralized strategies with no need for coordination between the sensors. We also present a case study in which we demonstrate an application of decentralized surveillance strategy synthesis. △ Less

Submitted 6 February, 2019; originally announced February 2019.

Journal ref: 2018 IEEE Conference on Decision and Control (CDC), FL, USA, 2018, pp. 3335-3342

Causality Analysis for Concurrent Reactive Systems (Extended Abstract)

Authors: Rayna Dimitrova, Rupak Majumdar, Vinayak S. Prabhu

Abstract: We present a comprehensive language theoretic causality analysis framework for explaining safety property violations in the setting of concurrent reactive systems. Our framework allows us to uniformly express a number of causality notions studied in the areas of artificial intelligence and formal methods, as well as define new ones that are of potential interest in these areas. Furthermore, our fo… ▽ More We present a comprehensive language theoretic causality analysis framework for explaining safety property violations in the setting of concurrent reactive systems. Our framework allows us to uniformly express a number of causality notions studied in the areas of artificial intelligence and formal methods, as well as define new ones that are of potential interest in these areas. Furthermore, our formalization provides means for reasoning about the relationships between individual notions which have mostly been considered independently in prior work; and allows us to judge the appropriateness of the different definitions for various applications in system design. In particular, we consider causality analysis notions for debugging, error resilience, and liability resolution in concurrent reactive systems. Finally, we present automata-based algorithms for computing various causal sets based on our language-theoretic encoding, and derive the algorithmic complexities. △ Less

Submitted 2 January, 2019; originally announced January 2019.

Comments: In Proceedings CREST 2018, arXiv:1901.00073

Journal ref: EPTCS 286, 2019, pp. 31-33

Maximum Realizability for Linear Temporal Logic Specifications

Authors: Rayna Dimitrova, Mahsa Ghasemi, Ufuk Topcu

Abstract: Automatic synthesis from linear temporal logic (LTL) specifications is widely used in robotic motion planning, control of autonomous systems, and load distribution in power networks. A common specification pattern in such applications consists of an LTL formula describing the requirements on the behaviour of the system, together with a set of additional desirable properties. We study the synthesis… ▽ More Automatic synthesis from linear temporal logic (LTL) specifications is widely used in robotic motion planning, control of autonomous systems, and load distribution in power networks. A common specification pattern in such applications consists of an LTL formula describing the requirements on the behaviour of the system, together with a set of additional desirable properties. We study the synthesis problem in settings where the overall specification is unrealizable, more precisely, when some of the desirable properties have to be (temporarily) violated in order to satisfy the system's objective. We provide a quantitative semantics of sets of safety specifications, and use it to formalize the "best-effort" satisfaction of such soft specifications while satisfying the hard LTL specification. We propose an algorithm for synthesizing implementations that are optimal with respect to this quantitative semantics. Our method builds upon the idea of the bounded synthesis approach, and we develop a MaxSAT encoding which allows for maximizing the quantitative satisfaction of the safety specifications. We evaluate our algorithm on scenarios from robotics and power distribution networks. △ Less

Submitted 2 April, 2018; originally announced April 2018.

Synthesis of surveillance strategies via belief abstraction

Authors: Suda Bharadwaj, Rayna Dimitrova, Ufuk Topcu

Abstract: We study the problem of synthesizing a controller for a robot with a surveillance objective, that is, the robot is required to maintain knowledge of the location of a moving, possibly adversarial target. We formulate this problem as a one-sided partial-information game in which the winning condition for the agent is specified as a temporal logic formula. The specification formalizes the surveillan… ▽ More We study the problem of synthesizing a controller for a robot with a surveillance objective, that is, the robot is required to maintain knowledge of the location of a moving, possibly adversarial target. We formulate this problem as a one-sided partial-information game in which the winning condition for the agent is specified as a temporal logic formula. The specification formalizes the surveillance requirement given by the user, including additional non-surveillance tasks. In order to synthesize a surveillance strategy that meets the specification, we transform the partial-information game into a perfect-information one, using abstraction to mitigate the exponential blow-up typically incurred by such transformations. This enables the use of off-the-shelf tools for reactive synthesis. We use counterexample-guided refinement to automatically achieve abstraction precision that is sufficient to synthesize a surveillance strategy. We evaluate the proposed method on two case-studies, demonstrating its applicability to large state-spaces and diverse requirements. △ Less

Submitted 19 March, 2018; v1 submitted 15 September, 2017; originally announced September 2017.

ACM Class: I.2.4

The Robot Routing Problem for Collecting Aggregate Stochastic Rewards

Authors: Rayna Dimitrova, Ivan Gavran, Rupak Majumdar, Vinayak S. Prabhu, Sadegh Esmaeil Zadeh Soudjani

Abstract: We propose a new model for formalizing reward collection problems on graphs with dynamically generated rewards which may appear and disappear based on a stochastic model. The *robot routing problem* is modeled as a graph whose nodes are stochastic processes generating potential rewards over discrete time. The rewards are generated according to the stochastic process, but at each step, an existing… ▽ More We propose a new model for formalizing reward collection problems on graphs with dynamically generated rewards which may appear and disappear based on a stochastic model. The *robot routing problem* is modeled as a graph whose nodes are stochastic processes generating potential rewards over discrete time. The rewards are generated according to the stochastic process, but at each step, an existing reward disappears with a given probability. The edges in the graph encode the (unit-distance) paths between the rewards' locations. On visiting a node, the robot collects the accumulated reward at the node at that time, but traveling between the nodes takes time. The optimization question asks to compute an optimal (or epsilon-optimal) path that maximizes the expected collected rewards. We consider the finite and infinite-horizon robot routing problems. For finite-horizon, the goal is to maximize the total expected reward, while for infinite horizon we consider limit-average objectives. We study the computational and strategy complexity of these problems, establish NP-lower bounds and show that optimal strategies require memory in general. We also provide an algorithm for computing epsilon-optimal infinite paths for arbitrary epsilon > 0. △ Less

Submitted 17 July, 2017; v1 submitted 18 April, 2017; originally announced April 2017.

Comments: 20 Pages. Full version of the CONCUR (28th International Conference on Concurrency Theory) 2017 paper

Proceedings Fifth Workshop on Synthesis

Authors: Ruzica Piskac, Rayna Dimitrova

Abstract: The SYNT workshop aims to bring together researchers interested in the broad area of synthesis of computing systems. The goal is to foster the development of frontier techniques in automating the development of computing system. Contributions of interest include algorithms, complexity and decidability analysis, as well as reproducible heuristics, implemented tools, and experimental evaluation. Ap… ▽ More The SYNT workshop aims to bring together researchers interested in the broad area of synthesis of computing systems. The goal is to foster the development of frontier techniques in automating the development of computing system. Contributions of interest include algorithms, complexity and decidability analysis, as well as reproducible heuristics, implemented tools, and experimental evaluation. Application domains include software, hardware, embedded, and cyberphysical systems. Computation models include functional, reactive, hybrid and timed systems. Identifying, formalizing, and evaluating synthesis in particular application domains is encouraged. The fifth iteration of the workshop took place in Toronto, Canada. It was co-located with the 28th International Conference on Computer Aided Verification. The workshop included twelve contributed talks and two invited talks. In addition, it featured a special session about the Syntax-Guided Synthesis Competition (SyGuS) and the SyntComp Synthesis competition. △ Less

Submitted 22 November, 2016; originally announced November 2016.

Journal ref: EPTCS 229, 2016

Reachability Analysis of Reversal-bounded Automata on Series-Parallel Graphs

Authors: Rayna Dimitrova, Rupak Majumdar

Abstract: Extensions to finite-state automata on strings, such as multi-head automata or multi-counter automata, have been successfully used to encode many infinite-state non-regular verification problems. In this paper, we consider a generalization of automata-theoretic infinite-state verification from strings to labeled series-parallel graphs. We define a model of non-deterministic, 2-way, concurrent aut… ▽ More Extensions to finite-state automata on strings, such as multi-head automata or multi-counter automata, have been successfully used to encode many infinite-state non-regular verification problems. In this paper, we consider a generalization of automata-theoretic infinite-state verification from strings to labeled series-parallel graphs. We define a model of non-deterministic, 2-way, concurrent automata working on series-parallel graphs and communicating through shared registers on the nodes of the graph. We consider the following verification problem: given a family of series-parallel graphs described by a context-free graph transformation system (GTS), and a concurrent automaton over series-parallel graphs, is some graph generated by the GTS accepted by the automaton? The general problem is undecidable already for (one-way) multi-head automata over strings. We show that a bounded version, where the automata make a fixed number of reversals along the graph and use a fixed number of shared registers is decidable, even though there is no bound on the sizes of series-parallel graphs generated by the GTS. Our decidability result is based on establishing that the number of context switches is bounded and on an encoding of the computation of bounded concurrent automata to reduce the emptiness problem to the emptiness problem for pushdown automata. △ Less

Submitted 23 September, 2015; originally announced September 2015.

Comments: In Proceedings GandALF 2015, arXiv:1509.06858

Journal ref: EPTCS 193, 2015, pp. 100-114

Approximate Counting in SMT and Value Estimation for Probabilistic Programs

Authors: Dmitry Chistikov, Rayna Dimitrova, Rupak Majumdar

Abstract: #SMT, or model counting for logical theories, is a well-known hard problem that generalizes such tasks as counting the number of satisfying assignments to a Boolean formula and computing the volume of a polytope. In the realm of satisfiability modulo theories (SMT) there is a growing need for model counting solvers, coming from several application domains (quantitative information flow, static ana… ▽ More #SMT, or model counting for logical theories, is a well-known hard problem that generalizes such tasks as counting the number of satisfying assignments to a Boolean formula and computing the volume of a polytope. In the realm of satisfiability modulo theories (SMT) there is a growing need for model counting solvers, coming from several application domains (quantitative information flow, static analysis of probabilistic programs). In this paper, we show a reduction from an approximate version of #SMT to SMT. We focus on the theories of integer arithmetic and linear real arithmetic. We propose model counting algorithms that provide approximate solutions with formal bounds on the approximation error. They run in polynomial time and make a polynomial number of queries to the SMT solver for the underlying theory, exploiting "for free" the sophisticated heuristics implemented within modern SMT solvers. We have implemented the algorithms and used them to solve the value problem for a model of loop-free probabilistic programs with nondeterminism. △ Less

Submitted 29 October, 2015; v1 submitted 3 November, 2014; originally announced November 2014.

Lossy Channel Games under Incomplete Information

Authors: Rayna Dimitrova, Bernd Finkbeiner

Abstract: In this paper we investigate lossy channel games under incomplete information, where two players operate on a finite set of unbounded FIFO channels and one player, representing a system component under consideration operates under incomplete information, while the other player, representing the component's environment is allowed to lose messages from the channels. We argue that these games are a s… ▽ More In this paper we investigate lossy channel games under incomplete information, where two players operate on a finite set of unbounded FIFO channels and one player, representing a system component under consideration operates under incomplete information, while the other player, representing the component's environment is allowed to lose messages from the channels. We argue that these games are a suitable model for synthesis of communication protocols where processes communicate over unreliable channels. We show that in the case of finite message alphabets, games with safety and reachability winning conditions are decidable and finite-state observation-based strategies for the component can be effectively computed. Undecidability for (weak) parity objectives follows from the undecidability of (weak) parity perfect information games where only one player can lose messages. △ Less

Submitted 4 March, 2013; originally announced March 2013.

Comments: In Proceedings SR 2013, arXiv:1303.0071

Journal ref: EPTCS 112, 2013, pp. 43-51