with C. Loeding and O. Serre.
Under submission.
The class of visibly pushdown languages has been recently defined as a subclass of context-free languages with desirable closure properties and tractable decision problems. We study visibly pushdown games, which are games played on visibly pushdown systems where the winning condition is given by a visibly pushdown language. We establish that, unlike pushdown games with pushdown winning conditions, visibly pushdown games are decidable and are 2Exptime-complete. We also show that pushdown games against LTL specifications and CARET specifications are 3Exptime-complete. Finally, we establish the topological complexity of visibly pushdown languages by showing that they are a subclass of Boolean combinations of Sigma_3 sets. This leads to an alternative proof that visibly pushdown automata are not determinizable and also shows that visibly pushdown games are determined.
with R. Alur and M. Bernadsky.
To appear in ICALP 2004.
Weighted timed automata are timed automata annotated with costs on locations and transitions. The optimal game-reachability problem for these automata is to find the best-cost strategy of supplying the inputs so as to ensure reachability of a target set within a specified number of iterations. The only known complexity bound for this problem is a doubly-exponential upper bound. We establish a singly-exponential upper bound and show that there exist automata with exponentially many states in a single region with pair-wise distinct optimal strategies.
with R. Alur.
To appear in STOC, Symp. on Theory of Computing, Chicago, 2004.
We propose the class of visibly pushdown languages as embeddings of context-free languages that is rich enough to model program analysis questions and yet is tractable and robust like the class of regular languages. In our definition, the input symbol determines when the pushdown automaton can push or pop, and thus the stack depth at every position. We show that the resulting class VPL of languages is closed under union, intersection, complementation, renaming, concatenation, and Kleene-*, and problems such as inclusion that are undecidable for context-free languages are EXPTIME-complete for visibly pushdown automata. Our framework explains, unifies, and generalizes many of the decision procedures in the program analysis literature, and allows algorithmic verification of recursive programs with respect to many context-free properties including access control properties via stack inspection and correctness of procedures with respect to pre and post conditions. We demonstrate that the class VPL is robust by giving two alternative characterizations: a logical characterization using the monadic second order (MSO) theory over words augmented with a binary matching predicate, and a correspondence to regular tree languages. We also consider visibly pushdown languages of infinite words and show that the closure properties, MSO-characterization and the characterization in terms of regular trees carry over. The main difference with respect to the case of finite words turns out to be determinizability: nondeterministic Buchi visibly pushdown automata are strictly more expressive than deterministic Muller automata.
with R. Alur and K. Etessami.
TACAS, Barcelona, Spain, 2004. LNCS © Springer-Verlag
Postscript
Model checking of linear temporal logic (LTL) specifications with respect to pushdown systems has been shown to be a useful tool for analysis of programs with potentially recursive procedures. LTL, however, can specify only regular properties, and properties such as correctness of procedures with respect to pre and post conditions, that require matching of calls and returns, are not regular. We introduce a
temporal logic of calls and returns CaRet for specification and algorithmic verification of correctness requirements of structured programs. The formulas of CaRet are interpreted over sequences of propositional valuations tagged with special symbolscall andret . Besides the standard global temporal modalities, CaRet admits theabstract-next operator that allows a path to jump from a call to thematching return. This operator can be used to specify a variety of non-regular properties such as partial and total correctness of program blocks with respect to pre and post conditions. The abstract versions of the other temporal modalities can be used to specify regular properties oflocal paths within a procedure that skip over calls to other procedures. CaRet also admits thecaller modality that jumps to the most recent pending call, and such caller modalities allow specification of a variety of security properties that involve inspection of the call-stack. Even though verifying context-free properties of pushdown systems is undecidable, we show that model checking CaRet formulas against a pushdown model is decidable. We present a tableau construction that reduces our model checking problem to the emptiness problem for a Buchi pushdown system. The complexity of model checking CaRet formulas is the same as that of checking LTL formulas, namely, polynomial in the model and singly exponential in the size of the specification.
with R. Alur and S. La Torre.
CONCUR, Marseilles, France, 2003, LNCS © Springer-Verlag
Postscript
Deciding 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. The previously known hardness proofs encode Turing machine computations using the next and/or until operators. Furthermore, in the case of model checking, disallowing next and until, and retaining only the always and eventually operators, lowers the complexity from PSPACE to NP. Whether such a reduction in complexity is possible for deciding games has been an open problem. In this paper, we provide a negative answer to this question. We introduce new techniques for encoding Turing machine computations using games, and show that deciding games for the LTL fragment with only the always and eventually operators is 2EXPTIME-hard. We also prove that if in this fragment we do not allow the eventually operator in the scope of the always operator and vice-versa, deciding games is EXPSPACE-hard, matching the previously known upper bound. On the positive side, we show that if the winning condition is a Boolean combination of formulas of the form "eventually p" and "infinitely often p," for a state-formula p, then the game can be decided in PSPACE, and also establish a matching lower bound. Such conditions include safety and reachability specifications on game graphs augmented with fairness conditions for the two players.
with Rajeev Alur and Wonhong Nam.
Bounded Model Checking Workshop, Boulder, Colorado, USA, 2003,
Postscript, PDF
We formulate and compare various symbolic computational techniques for deciding existence of winning strategies in two player games of perfect information. The game structure is given implicitly, and the winning condition is of the form "p until q" for state predicates p and q. The first technique employs symbolic fixpoint computation using ordered binary decision diagrams (BDDs). The second technique checks for the existence of strategies that ensure winning within k steps, for a user specified bound k, by reduction to the satisfiability of quantified boolean formulas. Finally, the bounded case can also be solved by reduction to satisfiability of ordinary boolean formulas, and we discuss two techniques, one based on encoding the strategy tree, and one based on encoding a witness subgraph, for reduction to SAT. We compare the various approaches on two examples using existing tools such as Mucke, Mocha, Semprop, Quaffle, Qube, Berkmin and zChaff.
with R. Alur and S. La Torre.
CAV, Boulder, Colorado, USA, 2003, LNCS © Springer-Verlag
Postscript
This paper is a sequel to the paper below in TACAS'03, and we consider modular strategies on recursive game graphs but now with external winning conditions and omega-regular winning conditions. We first consider the case when the specification is given as a deterministic Buchi 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-Buchi 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.
with Deepak D'Souza, Patricia Bouyer and Antoine Petit.
CAV, Boulder, Colorado, USA, 2003, LNCS © Springer-Verlag
Postscript
This paper is a sequel to the paper on timed control in STACS'02. We consider the problem of synthesizing controllers for timed systems modeled using timed automata. The point of departure from earlier work is that we consider controllers that have only a partial observation of the system that it controls. In discrete event systems (where continuous time is not modeled), it is well known how to handle partial observability, and decidability issues do not differ from the complete information setting. We show however that timed control under partial observability is undecidable even for internal specifications (while the analogous problem under complete observability is decidable) and we identify a decidable subclass.
LICS, Ottawa, Canada, 2003, © IEEE
Postscript
Given a regular collection of Mazurkiewicz traces, which can be seen as the behaviours of a finite-state concurrent system, one can associate with it a canonical regular event structure. This event structure is a single (often infinite) structure that captures both the concurrency and conflict information present in the system. We study the problem of model-checking such structures against logics such as first-order logic (FOL), monadic second-order logic (MSOL) and a new logic that lies in between these two called monadic trace logic (MTL). MTL is a fragment of MSOL where the quantification is restricted to sets that are conflict-free. While it is known that model-checking such event structures against MSOL is undecidable, our main results are that FOL and MTL admit effective model-checking procedures. It turns out that FOL captures previously known decidable temporal logics on event structures. MTL is more powerful and can express interesting branching-time properties of event structures, and when restricted to a sequential setting, can express the standard logic CTL* over trees.
with R. Alur and S. La Torre.
9th TACAS, Warsaw, Poland, 2003, LNCS © Springer-Verlag
Postscript
In this paper, we focus on solving games in recursive game graphs that 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 fixpoint computation algorithm for solving modular games such that the worst-case 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.
with M. Leucker and S. Mukhopadhyay.
22nd FSTTCS, Kanpur, India, 2002, LNCS © Springer-Verlag
Postscript
We introduce a formalism to specify classes of MSCs over an unbounded number of processes. The formalism can describe many interesting behaviours of dynamically changing networks of processes. Moreover, it strictly includes the formalism of Message Sequence Graphs studied in the literature to describe MSCs over a fixed finite set of processes. Our main result is that model-checking of MSCs described in this formalism against a suitable monadic-second order logic is decidable.
with P.S. Thiagarajan.
CONCUR, Brno, Czech Republic, 2002, LNCS 2421 © Springer-Verlag
Postscript
We study the problem of synthesizing controllers in a natural distributed asynchronous setting: a finite set of plants interact with their local environments and communicate with each other by synchronizing on common actions. The controller-synthesis problem is to come up with a local strategy for each plant such that the controlled behaviour of the network meets a specification. We consider linear time specifications and provide, in some sense, a minimal set of restrictions under which this problem is effectively solvable: we show that the controller-synthesis problem under these restrictions is decidable while the problem becomes undecidable if any one or more of these three restrictions are dropped.
with Deepak D'Souza, CMI.
STACS, Antibes - Juan les Pins, France, 2002, LNCS 2285 © Springer-Verlag
Postscript
We study the problem of control synthesis for a timed plant and an external timed specification, modelled as timed automata. Our main result is that the problem is decidable when we are given a priori the resources for the controller (the number of clocks, observational power of clocks, etc.) and when the specification is an $\omega$-regular timed language describing undesired behaviours. We also show that for deterministic specifications, if there is a controller at all, then there is one which uses the combined resources of the plant and specification. The decidability of other related problems is also investigated.
with P.S. Thiagarajan, CMI.
CONCUR '98 Special Issue, Theoretical Computer Science, 274 1-2 (2002) © Elsevier Sceince
Postscript, PDF (actual journal version)
This is the journal version of the paper below. The problem for sequential transition systems is extended to the case of bisimulations and shown to be solvable in polynomial time.
Ph.D. thesis, November 2001
Postscript
This thesis contains the work on control and synthesis reported in the papers below. It has control-synthesis for simulations and bisimulations, undecidability of checking for asynchronous simulations, synthesis and control for branching-time specifications against reactive environments and distributed control for local specifications.
with B. Meenakshi.
21st FSTTCS, Bangalore, India, 2001, LNCS 2245 © Springer-Verlag
Postscript
We study the model-checking problem for classes of message sequence charts (MSCs) defined by two extensions of message sequence graphs (MSGs). These classes subsume the class of regular MSC languages. We show that the model checking problem for these extended message sequence graphs against monadic second-order specifications is decidable. Moreover, we present two ways to model-check the extended classes --- one extends the proof for MSGs while the other extends the proof for regular MSC languages.
28th ICALP, Crete, Greece, 2001, LNCS 2076 © Springer-Verlag
Postscript
We study the model-checking problem of message-sequence graphs (MSGs). In the sequential setting, we consider the set of message-sequence charts (MSCs) represented by an MSG and tackle specifications given in monadic second-order logic. We show that this problem, without any restrictions on the MSGs, is decidable. We then turn to branching behaviours of MSGs, define a notion of an unfolding of an MSG, and show that the model-checking problem on unfoldings is also decidable. Our results are stronger and imply that, over an appropriate universe, satisfiability and synthesis of MSCs and MSGs, respectively, are decidable.
with P.S. Thiagarajan.
28th ICALP, Crete, Greece, 2001, LNCS 2076 © Springer-Verlag
Postscript
We consider the problem of synthesizing distributed controllers for reactive systems against local specifications. We show that a larger class of architectures become decidable in comparison to the analogous problem for global specifications. We identify the exact class of architectures for which the problem is decidable. Our results also show the decidability of a related realizability problem for local specifications.
with O. Kupferman, P.S. Thiagarajan, M. Vardi.
11th CONCUR, Penn. State Univ., USA, 2000, LNCS 1877 © Springer-Verlag
Postscript
We consider the problem of synthesizing systems which react with environments that can offer arbitrary sets of moves as possible moves it can make. Such environments are required if one wants to do modular synthesis against branching-time specifications. We show that the synthesis and control-synthesis problems are 2EXPTIME-complete (3EXPTIME-complete) for CTL (CTL*).
with P.S. Thiagarajan, CMI.
9th CONCUR, Nice, France, 1998, LNCS 1466 © Springer-Verlag
Postscript
This paper introduces the problem of studying controllers for branching-time specifications; the specification is that the behaviour should be simulated by a transition system. The problem is shown to be decidable for sequential transition systems and (surprisingly) undecidable for asychronous transition systems.
with Deepak D'Souza, CMI.
National Seminar on Theoretical Computer Science, Madras, June '97.
Postscript
This is an extension of the work below, exhibiting an algorithm which generates distributed automata on-the-fly for verification against Product-LTL formulas.
M.Sc. thesis, 1994
Postscript
Centered around a paper by Gerth, Peled, Vardi and Wolper on an on-the-fly algorithm for LTL, this report generalizes their algorithm to LTL enriched with actions, and gives a cleaner proof of correctness.