720 research outputs found
Expressiveness of streaming string transducers
No full textStreaming string transducers define (partial) functions from input strings to output strings. A streaming string transducer makes a single pass through the input string and uses a finite set of variables that range over strings from the output alphabet. At every step, the transducer processes an input symbol, and updates all the variables in parallel using assignments whose right-hand-sides are concatenations of output symbols and variables with the restriction that a variable can be used at most once in a right-hand-side expression. It has been shown that streaming string transducers operating on strings over infinite data domains are of interest in algorithmic verification of list-processing programs, as they lead to Pspace decision procedures for checking pre/postconditions and for checking semantic equivalence, for a well-defined class of heap-manipulating programs. In order to understand the theoretical expressiveness of streaming transducers, we focus on streaming transducers processing strings over finite alphabets, given the existence of a robust and well-studied class of ``regular'' transductions for this case. Such regular transductions can be defined either by two-way deterministic finite-state transducers, or using a logical MSO-based characterization. Our main result is that the expressiveness of streaming string transducers coincides exactly with this class of regular transductions
Automata-Based Stream Processing
No full textWe propose an automata-theoretic framework for modularly expressing computations on streams of data. With weighted automata as a starting point, we identify three key features that are useful for an automaton model for stream processing: expressing the regular decomposition of streams whose data items are elements of a complex type (e.g., tuple of values), allowing the hierarchical nesting of several different kinds of aggregations, and specifying modularly the parallel execution and combination of various subcomputations. The combination of these features leads to subtle efficiency considerations that concern the interaction between nondeterminism, hierarchical nesting, and parallelism. We identify a syntactic restriction where the nondeterminism is unambiguous and parallel subcomputations synchronize their outputs. For automata satisfying these restrictions, we show that there is a space- and time-efficient streaming evaluation algorithm. We also prove that when these restrictions are relaxed, the evaluation problem becomes inherently computationally expensive
Hedging Bets in Markov Decision Processes
No full textThe classical model of Markov decision processes with costs or rewards, while widely used to formalize optimal decision making, cannot capture scenarios where there are multiple objectives for the agent during the system evolution, but only one of these objectives gets actualized upon termination. We introduce the model of Markov decision processes with alternative objectives (MDPAO) for formalizing optimization in such scenarios. To compute the strategy to optimize the expected cost/reward upon termination, we need to figure out how to balance the values of the alternative objectives. This requires analysis of the underlying infinite-state process that tracks the accumulated values of all the objectives. While the decidability of the problem of computing the exact optimal strategy for the general model remains open, we present the following results. First, for a Markov chain with alternative objectives, the optimal expected cost/reward can be computed in polynomial-time. Second, for a single-state process with two actions and multiple objectives we show how to compute the optimal decision strategy. Third, for a process with only two alternative objectives, we present a reduction to the minimum expected accumulated reward problem for one-counter MDPs, and this leads to decidability for this case under some technical restrictions. Finally, we show that optimal cost/reward can be approximated up to a constant additive factor for the general problem
Regular Transformations (Dagstuhl Seminar 23202)
No full textThis report documents the program and the outcomes of the Dagstuhl Seminar 23202 "Regular Transformations". The goal of this seminar was to advance on a list of topics about transducers that have gathered much interest recently, and to explore new connections between the theory of regular transformations and its applications in linguistics
A generic approach for the automatic verification of featured, parameterised systems
No full textA general technique is presented that allows property based feature analysis of systems consisting of an arbitrary number of components. Each component may have an arbitrary set of safe features. The components are defined in a guarded command form and the technique combines model checking and abstraction. Features must fulfill certain criteria in order to be safe, the criteria express constraints on the variables which occur in feature guards. The main result is a generalisation theorem which we apply to a well known example: the ubiquitous, featured telephone system
Deterministic generators and games for ltl fragments
No full textDeciding infinite two-player games on finite graphs with the winning condition specified by a linear temporal logic (Ltl) formula, is known to be 2Exptime-complete. In this paper, we identify Ltl fragments of lower complexity. Solving Ltl games typically involves a doubly exponential translation from Ltl formulas to deterministic ω-automata. First, we show that the longest distance (length of the longest simple path) of the generator is also an important parameter, by giving an O(d log n)-space procedure to solve a Büchi game on a graph with n vertices and longest distance d. Then, for the Ltl fragment of the boolean combinations of formulas obtained only by eventualities and conjunctions, we provide a translation to deterministic generators of exponential size and linear longest distance, show both of these bounds to be optimal, and prove the corresponding games to be Pspace-complete. Introducing next modalities in this fragment, we give a translation to deterministic generators still of exponential size but also with exponential longest distance, show both of these bounds to be optimal, and prove the corresponding games to be Exptime-complete. For the fragment resulting by further adding disjunctions, we provide a translation to deterministic generators of doubly exponential size and exponential longest distance, show both of these bounds to be optimal, and prove the corresponding games to be Expspace. W
하이브리드 시스템의 정형 모델링 및 분석: 다수의 로봇 조종 사례연구
No full textThe design of controllers for hybrid systems (i.e. mixed discrete-continuous systems) in a systematic manner remains a challenging task. In this case study, we apply formal modeling to the design of communication and control strategies for a team of autonomous robots to attain specified goals in a coordinated manner. The model of linear hybrid automata is used to describe the high-level design, and the verification software HYTECH is used for symbolic analysis of the description. The goal of the project is to understand tradeoffs among various design alternatives by generating constraints among parameters using symbolic analysis. In this paper, we report on diffculties in modeling a team of robots using linear hybrid automata, results of analysis experiments, promise of the approach, and challenges for future research.We gratefully acknowledge the support of NSF grant
CISE CDS 97-03220-001,NSF CAREER award CCR-9734115,NSF CCR-9619910,
ARO DAAG55-98-1-0393, ARO DAAG55-98-1-0466, ONR N00014-97-1-0505
and the DARPA ITO/MARS program. J. Esposito was supported by a De-
partment of Education fellowship
Verifying Abstractions of Timed Systems
No full textions of Timed Systems Serdar Ta¸siran ? Rajeev Alur ?? Robert P. Kurshan ?? Robert K. Brayton ? Abstract. Given two descriptions of a real-time system at different levels of abstraction, we consider the problem of proving that the refined representation is a correct implementation of the abstract one. To avoid the complexity of building a representation for the refined system in its entirety, we develop a compositional framework for the implementation check to be carried out in a module-by-module manner using assumeguarantee style proof rules. On the algorithmic side, we show that the problem of checking for timed simulation relations, a sufficient condition for correct implementation, is decidable. We study state homomorphisms as a way of specifying a correspondence between two modules. We present an algorithm for checking if a given mapping is a homomorphism preserving timed behaviors. We have implemented this check in the verifier Cospan, and applied our method to the comp..
Modular Strategies for Recursive Game Graphs
No full textMany problems in formal verification and program analysis can be formalized as computing winning strategies for two-player games on graphs. In this paper, we focus on solving games in recursive game graphs which can model the control flow in sequential programs with recursive procedure calls. While such games can be viewed as the pushdown games studied in the literature, the natural notion of winning in our framework requires the strategies to be modular with only local memory; that is, resolution of choices within a module does not depend on the context in which the module is invoked, but only on the history within the current invocation of the module. While reachability in (global) pushdown games is known to be EXPTIME-complete, we show reachability in modular games to be NP-complete. We present a fixed-point computation algorithm for solving modular games such that in the worst case the number of iterations is exponential in the total number of returned values from the modules. If the strategy within a module does not depend on the global history, but can remember the history of the past invocations of this module, that is, if memory is local but persistent, we show that reachability becomes undecidable
Modular Strategies for Infinite Games on Recursive Graphs
No full textIn this paper, we focus on solving games in recursive game graphs that can model the control flow of sequential programs with recursive procedure calls. The winning condition is given as an ω-regular specification over the observable, and, unlike traditional pushdown games, the strategy is required to be modular: resolution of choices within a component should not depend on the context in which the component is invoked, but only on the history within the current invocation of the component. We first consider the case when the specification is given as a deterministic Büchi automaton. We show the problem to be decidable, and present a solution based on two-way alternating tree automata with time complexity that is polynomial in the number of internal nodes, exponential in the specification and exponential in the number of exits of the components. We show that the problem is EXPTIME-complete in general, and NP-complete for fixed-size specifications. Then, we show that the same complexity bounds apply if the specification is given as a universal co-Büchi automaton. Finally, for specifications given as formulas of linear temporal logic LTL, we obtain a synthesis algorithm that is doubly-exponential in the formula and singly exponential in the number of exits of components
- …
