@inproceedings{3873, abstract = {We study the controller synthesis problem under budget constraints. In this problem, there is a cost associated with making an observation, and a controller can make only a limited number of observations in each round so that the total cost of the observations does not exceed a given fixed budget. The controller must ensure some omega-regular requirement subject to the budget constraint. Budget constraints arise in designing and implementing controllers for resource-constrained embedded systems, where a controller may not have enough power, time, or bandwidth to obtain data from all sensors in each round. They lead to games of imperfect information, where the unknown information is not fixed a priori, but can vary from round to round, based on the choices made by the controller how to allocate its budget. We show that the budget-constrained synthesis problem for W-regular objectives is complete for exponential time. In addition to studying synthesis under a fixed budget constraint, we study the budget optimization problem, where given a plant, an objective, and observation costs, we have to find a controller that achieves the objective with minimal average accumulated cost (or minimal peak cost). We show that this problem is reducible to a game of imperfect information where the winning objective is a conjunction of an omega-regular condition and a long-run average condition (or a least max-cost condition), and this again leads to an exponential-time algorithm. Finally, we extend our results to games over infinite state spaces, and show that the budget-constrained synthesis problem is decidable for infinite state games with stable quotients of finite index. Consequently, the discrete time budget-constrained synthesis problem is decidable for rectangular hybrid automata.}, author = {Chatterjee, Krishnendu and Majumdar, Ritankar and Henzinger, Thomas A}, booktitle = {11th Workshop on Hybrid Systems: Computation and Control}, issn = {1611-3349}, location = {St. Louis, MO, United States}, pages = {72 -- 86}, publisher = {Springer Nature}, title = {{Controller synthesis with budget constraints}}, doi = {DOI: 10.1007/978-3-540-78929-1_6}, volume = {4981}, year = {2008}, } @inproceedings{3874, abstract = {We consider concurrent two-player timed automaton games with omega-regular objectives specified as parity conditions. These games offer an appropriate model for the synthesis of real-time controllers. Earlier works on timed games focused on pure strategies for each player. We study, for the first time, the use of randomized strategies in such games. While pure (i.e., nonrandomized) strategies in timed games require infinite memory for winning even with respect to reachability objectives, we show that randomized strategies can win with finite memory with respect to all parity objectives. Also, the synthesized randomized real-time controllers are much simpler in structure than the corresponding pure controllers, and therefore easier to implement. For safety objectives we prove the existence of pure finite-memory winning strategies. Finally, while randomization helps in simplifying the strategies required for winning timed parity games, we prove that randomization does not help in winning at more states.}, author = {Chatterjee, Krishnendu and Henzinger, Thomas A and Prabhu, Vinayak}, booktitle = {11th Workshop on Hybrid Systems: Computation and Control}, issn = {1611-3349}, location = {St. Louis, MO, United States}, pages = {87 -- 100}, publisher = {Springer Nature}, title = {{Trading infinite memory for uniform randomness in timed games}}, doi = {10.1007/978-3-540-78929-1_7}, volume = {4981}, year = {2008}, } @inproceedings{3875, abstract = {We study the problem of model checking Interval-valued Discrete-time Markov Chains (IDTMC). IDTMCs are discrete-time finite Markov Chains for which the exact transition probabilities are riot known. Instead in IDTMCs, each transition is associated with an interval in which the actual transition probability must lie. We consider two semantic interpretations for the uncertainty in the transition probabilities of an IDTMC. In the first interpretation, we think of an IDTMC as representing a (possibly uncountable) family of (classical) discrete-time Markov Chains, where each member of the family is a Markov Chain whose transition probabilities lie within the interval range given in the IDTMC. We call this semantic interpretation Uncertain Markov Chains (UMC). In the second semantics for an IDTMC, which we call Interval Markov Decision Process (IMDP), we view the uncertainty as being resolved through non-determinism. In other words, each time a state is visited, we adversarially pick a transition distribution that respects the interval constraints, and take a probabilistic step according to the chosen distribution. We introduce a logic omega-PCTL that can express liveness, strong fairness, and omega-regular properties (such properties cannot be expressed in PCTL). We show that the omega-PCTL model checking problem for Uncertain Markov Chain semantics is decidable in PSPACE (same as the best known upper bound for PCTL) and for Interval Markov Decision Process semantics is decidable in coNP (improving the previous known PSPACE bound for PCTL). We also show that the qualitative fragment of the logic can lie solved in coNP for the UMC interpretation, and can be solved in polynomial time for a sub-class of UMCs. We also prove lower bounds for these model checking problems. We show that the model checking problem of IDTMCs with LTL formulas can be solved for both UMC and IMDP semantics by reduction to the model checking problem of IDTMC with omega-PcTL formulas.}, author = {Chatterjee, Krishnendu and Henzinger, Thomas A and Sen, Koushik}, booktitle = {Foundations of Software Science and Computational Structures - 11th International Conference}, issn = {1611-3349}, location = {Budapest, Hungary}, pages = {302 -- 317}, publisher = {Springer Nature}, title = {{Model-checking omega-regular properties of interval Markov chains}}, doi = {10.1007/978-3-540-78499-9_22}, volume = {4962}, year = {2008}, } @inproceedings{3877, abstract = {The synthesis problem asks to construct a reactive finite-state system from an omega-regular specification. Initial specifications are often unrealizable, which means that there is no system that implements the specification. A common reason for unrealizability is that assumptions on the environment of the system are incomplete. We study the problem of correcting an unrealizable specification phi by computing an environment assumption psi such that the new specification psi -> phi is realizable. Our aim is to construct an assumption psi that constrains only the environment and is as weak as possible. We present a two-step algorithm for computing assumptions. The algorithm operates on the game graph that is used to answer the realizability question. First, we compute a safety assumption that removes a minimal set of environment edges from the graph. Second, we compute a liveness assumption that puts fairness conditions on some of the remaining environment edges. We show that the problem of finding a minimal set of fair edges is computationally hard, and we use probabilistic games to compute a locally minimal fairness assumption.}, author = {Chatterjee, Krishnendu and Henzinger, Thomas A and Jobstmann, Barbara}, booktitle = {19th International Conference on Concurrency Theory}, issn = {1611-3349}, location = {Toronto, Canada}, pages = {147 -- 161}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Environment assumptions for synthesis}}, doi = {10.1007/978-3-540-85361-9_14}, volume = {5201}, year = {2008}, } @inproceedings{3878, abstract = {We study the problem of generating a test sequence that achieves maximal coverage for a reactive system under test. We formulate the problem as a repeated game between the tester and the system, where the system state space is partitioned according to some coverage criterion and the objective of the tester is to maximize the set of partitions (or coverage goals) visited during the game. We show the complexity of the maximal coverage problem for non-deterministic systems is PSPACE-complete, but is NP-complete for deterministic systems. For the special case of non-deterministic systems with a re-initializing “reset” action, which represent running a new test input on a re-initialized system, we show that the complexity is coNP-complete. Our proof technique for reset games uses randomized testing strategies that circumvent the exponentially large memory requirement of deterministic testing strategies.}, author = {Chatterjee, Krishnendu and De Alfaro, Luca and Majumdar, Ritankar}, booktitle = {6th Asian Symposium on Programming Language and Systems}, issn = {1611-3349}, location = {Bangalore, India}, pages = {91 -- 106}, publisher = {Springer Nature}, title = {{The complexity of coverage}}, doi = {10.1007/978-3-540-89330-1_7}, volume = {5356}, year = {2008}, } @inproceedings{3879, abstract = {Quantitative generalizations of classical languages, which assign to each word a real number instead of a boolean value, have applications in modeling resource-constrained computation. We use weighted automata (finite automata with transition weights) to define several natural classes of quantitative languages over finite and infinite words; in particular, the real value of an infinite run is computed as the maximum, limsup, liminf, limit average, or discounted sum of the transition weights. We define the classical decision problems of automata theory (emptiness, universality, language inclusion, and language equivalence) in the quantitative setting and study their computational complexity. As the decidability of language inclusion remains open for some classes of weighted automata, we introduce a notion of quantitative simulation that is decidable and implies language inclusion. We also give a complete characterization of the expressive power of the various classes of weighted automata. In particular, we show that most classes of weighted automata cannot be determinized.}, author = {Chatterjee, Krishnendu and Doyen, Laurent and Henzinger, Thomas A}, booktitle = {22nd International Workshop on Computer Science Logic}, issn = {1611-3349}, location = {Bertinoro, Italy}, pages = {385 -- 400}, publisher = {Springer Nature}, title = {{Quantitative languages}}, doi = {10.1007/978-3-540-87531-4_28}, volume = {5213}, year = {2008}, } @inproceedings{3880, abstract = {We consider imperfect-information parity games in which strategies rely on observations that provide imperfect information about the history of a play. To solve such games, i.e., to determine the winning regions of players and corresponding winning strategies, one can use the subset construction to build an equivalent perfect-information game. Recently, an algorithm that avoids the inefficient subset construction has been proposed. The algorithm performs a fixed-point computation in a lattice of antichains, thus maintaining a succinct representation of state sets. However, this representation does not allow to recover winning strategies. In this paper, we build on the antichain approach to develop an algorithm for constructing the winning strategies in parity games of imperfect information. We have implemented this algorithm as a prototype. To our knowledge, this is the first implementation of a procedure for solving imperfect-information parity games on graphs.}, author = {Berwanger, Dietmar and Chatterjee, Krishnendu and Doyen, Laurent and Henzinger, Thomas A and Raje, Sangram}, booktitle = {19th International Conference, CONCUR 2008}, issn = {1611-3349}, location = {Toronto, Canada}, pages = {325 -- 339}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Strategy construction for parity games with imperfect information}}, doi = {10.1007/978-3-540-85361-9}, volume = {5201}, year = {2008}, } @inproceedings{3876, abstract = {We consider two-player games played in real time on game structures with clocks and parity objectives. The games are concurrent in that at each turn, both players independently propose a time delay and an action, and the action with the shorter delay is chosen. To prevent a player from winning by blocking time, we restrict each player to strategies that ensure that the player cannot be responsible for causing a zeno run. First, we present an efficient reduction of these games to turn-based (i.e., nonconcurrent) finite-state (i.e., untimed) parity games. The states of the resulting game are pairs of clock regions of the original game. Our reduction improves the best known complexity for solving timed parity games. Moreover, the rich class of algorithms for classical parity games can now be applied to timed parity games. Second, we consider two restricted classes of strategies for the player that represents the controller in a real-time synthesis problem, namely, limit-robust and bounded-robust strategies. Using a limit-robust strategy, the controller cannot choose an exact real-valued time delay but must allow for some nonzero jitter in each of its actions. If there is a given lower bound on the jitter, then the strategy is bounded-robust. We show that exact strategies are more powerful than limit-robust strategies, which are more powerful than bounded-robust strategies for any bound. For both kinds of robust strategies, we present efficient reductions to standard timed automaton games. These reductions provide algorithms for the synthesis of robust real-time controllers.}, author = {Chatterjee, Krishnendu and Henzinger, Thomas A and Prabhu, Vinayak}, booktitle = {Proceedings of the 6th international conference on Formal Modeling and Analysis of Timed Systems}, isbn = {9783540857778}, issn = {1611-3349}, location = {Saint Malo, France}, pages = {124 -- 140}, publisher = {Springer Nature}, title = {{Timed parity games: complexity and robustness}}, doi = {10.1007/978-3-540-85778-5_10}, volume = {5215}, year = {2008}, } @inproceedings{18320, abstract = {Presented here is the problem of recovering a dynamic image superimposed on a static background. Such a problem is ill-posed and may arise e.g. in imaging through semireflective media, in separation of an illumination image from a reflectance image, in imaging with diffraction phenomena, etc. In this work we study regularization of this problem in spirit of Total Variation and general sparsifying transformations.}, author = {Bronstein, Alexander and Bronstein, Michael M. and Zibulevsky, Michael}, booktitle = {6th International Conference on Independent Component Analysis and Signal Separation}, isbn = {9783540326304}, issn = {1611-3349}, location = {Charleston, SC, United States}, pages = {934--940}, publisher = {Springer Nature}, title = {{On separation of semitransparent dynamic images from static background}}, doi = {10.1007/11679363_116}, volume = {3889}, year = {2006}, } @inproceedings{18321, abstract = {Recent studies on three-dimensional face recognition proposed to model facial expressions as isometries of the facial surface. Based on this model, expression-invariant signatures of the face were constructed by means of approximate isometric embedding into flat spaces. Here, we apply a new method for measuring isometry-invariant similarity between faces by embedding one facial surface into another. We demonstrate that our approach has several significant advantages, one of which is the ability to handle partially missing data. Promising face recognition results are obtained in numerical experiments even when the facial surfaces are severely occluded.}, author = {Bronstein, Alexander and Bronstein, Michael M. and Kimmel, Ron}, booktitle = {9th European Conference on Computer Vision}, isbn = {9783540338369}, issn = {1611-3349}, location = {Graz, Austria}, publisher = {Springer Nature}, title = {{Robust expression-invariant face recognition from partially missing data}}, doi = {10.1007/11744078_31}, volume = {3953}, year = {2006}, } @inproceedings{18322, abstract = {A geometric framework for finding intrinsic correspondence between animated 3D faces is presented. We model facial expressions as isometries of the facial surface and find the correspondence between two faces as the minimum-distortion mapping. Generalized multidimensional scaling is used for this goal. We apply our approach to texture mapping onto 3D video, expression exaggeration and morphing between faces.}, author = {Bronstein, Alexander and Bronstein, Michael M. and Kimmel, Ron}, booktitle = {4th International Conference on Articulated Motion and Deformable Objects}, isbn = {9783540360315}, issn = {1611-3349}, location = {Mallorca, Spain}, pages = {38--47}, publisher = {Springer Nature}, title = {{Facetoface: An isometric model for facial animation}}, doi = {10.1007/11789239_5}, volume = {4069}, year = {2006}, } @inproceedings{18323, abstract = {We present a theoretical and computational framework for matching of two-dimensional articulated shapes. Assuming that articulations can be modeled as near-isometries, we show an axiomatic construction of an articulation-invariant distance between shapes, formulated as a generalized multidimensional scaling (GMDS) problem and solved efficiently. Some numerical results demonstrating the accuracy of our method are presented.}, author = {Bronstein, Alexander and Bronstein, Michael M. and Bruckstein, Alfred M. and Kimmel, Ron}, booktitle = {4th International Conference on Articulated Motion and Deformable Objects}, isbn = {9783540360315}, issn = {1611-3349}, location = {Mallorca, Spain}, pages = {48--57}, publisher = {Springer Nature}, title = {{Matching two-dimensional articulated shapes using generalized multidimensional scaling}}, doi = {10.1007/11789239_6}, volume = {4069}, year = {2006}, } @inproceedings{4551, abstract = {We consider Markov decision processes (MDPs) with multiple discounted reward objectives. Such MDPs occur in design problems where one wishes to simultaneously optimize several criteria, for example, latency and power. The possible trade-offs between the different objectives are characterized by the Pareto curve. We show that every Pareto-optimal point can be achieved by a memoryless strategy; however, unlike in the single-objective case, the memoryless strategy may require randomization. Moreover, we show that the Pareto curve can be approximated in polynomial time in the size of the MDP. Additionally, we study the problem if a given value vector is realizable by any strategy, and show that it can be decided in polynomial time; but the question whether it is realizable by a deterministic memoryless strategy is NP-complete. These results provide efficient algorithms for design exploration in MDP models with multiple objectives. This research was supported in part by the AFOSR MURI grant F49620-00-1-0327, and the NSF grants CCR-0225610, CCR-0234690, and CCR-0427202. }, author = {Chatterjee, Krishnendu and Majumdar, Ritankar and Henzinger, Thomas A}, booktitle = {Proceedings of the 23rd Annual conference on Theoretical Aspects of Computer Science}, isbn = {9783540323013}, issn = {0302-9743}, location = {Marseille, France}, pages = {325 -- 336}, publisher = {Springer}, title = {{Markov decision processes with multiple objectives}}, doi = {10.1007/11672142_26}, volume = {3884}, year = {2006}, } @inproceedings{4538, abstract = {A stochastic graph game is played by two players on a game graph with probabilistic transitions. We consider stochastic graph games with ω-regular winning conditions specified as parity objectives. These games lie in NP ∩ coNP. We present a strategy improvement algorithm for stochastic parity games; this is the first non-brute-force algorithm for solving these games. From the strategy improvement algorithm we obtain a randomized subexponential-time algorithm to solve such games.}, author = {Chatterjee, Krishnendu and Henzinger, Thomas A}, booktitle = {Proceedings of the 23rd Annual conference on Theoretical Aspects of Computer Science}, isbn = {9783540323013}, issn = {1611-3349}, location = {Marseille, France}, pages = {512 -- 523}, publisher = {Springer}, title = {{Strategy improvement and randomized subexponential algorithms for stochastic parity games}}, doi = {10.1007/11672142_42}, volume = {3884}, year = {2006}, } @inproceedings{4437, abstract = {The synthesis of reactive systems requires the solution of two-player games on graphs with ω-regular objectives. When the objective is specified by a linear temporal logic formula or nondeterministic Büchi automaton, then previous algorithms for solving the game require the construction of an equivalent deterministic automaton. However, determinization for automata on infinite words is extremely complicated, and current implementations fail to produce deterministic automata even for relatively small inputs. We show how to construct, from a given nondeterministic Büchi automaton, an equivalent nondeterministic parity automaton that is good for solving games with objective . The main insight is that a nondeterministic automaton is good for solving games if it fairly simulates the equivalent deterministic automaton. In this way, we omit the determinization step in game solving and reactive synthesis. The fact that our automata are nondeterministic makes them surprisingly simple, amenable to symbolic implementation, and allows an incremental search for winning strategies.}, author = {Henzinger, Thomas A and Piterman, Nir}, booktitle = {Proceedings of the 20th international conference on Computer Science Logic}, isbn = {9783540454588}, issn = {1611-3349}, location = {Szeged, Hungary}, pages = {395 -- 410}, publisher = {Springer}, title = {{Solving games without determinization}}, doi = {10.1007/11874683_26}, volume = {4207}, year = {2006}, } @inproceedings{4406, abstract = {We propose and evaluate a new algorithm for checking the universality of nondeterministic finite automata. In contrast to the standard algorithm, which uses the subset construction to explicitly determinize the automaton, we keep the determinization step implicit. Our algorithm computes the least fixed point of a monotone function on the lattice of antichains of state sets. We evaluate the performance of our algorithm experimentally using the random automaton model recently proposed by Tabakov and Vardi. We show that on the difficult instances of this probabilistic model, the antichain algorithm outperforms the standard one by several orders of magnitude. We also show how variations of the antichain method can be used for solving the language-inclusion problem for nondeterministic finite automata, and the emptiness problem for alternating finite automata.}, author = {De Wulf, Martin and Doyen, Laurent and Henzinger, Thomas A and Raskin, Jean}, booktitle = {Proceedings of the 18th international conference on Computer Aided Verification}, isbn = {9783540374060}, issn = {1611-3349}, location = {Seattle, WA, United States}, pages = {17 -- 30}, publisher = {Springer Nature}, title = {{Antichains: A new algorithm for checking universality of finite automata}}, doi = {10.1007/11817963_5}, volume = {4144}, year = {2006}, } @inproceedings{4432, abstract = {We add freeze quantifiers to the game logic ATL in order to specify real-time objectives for games played on timed structures. We define the semantics of the resulting logic TATL by restricting the players to physically meaningful strategies, which do not prevent time from diverging. We show that TATL can be model checked over timed automaton games. We also specify timed optimization problems for physically meaningful strategies, and we show that for timed automaton games, the optimal answers can be approximated to within any degree of precision.}, author = {Henzinger, Thomas A and Prabhu, Vinayak}, booktitle = {Proceedings of the 4th international conference on Formal Modeling and Analysis of Timed Systems}, isbn = {9783540450269}, issn = {1611-3349}, location = {Paris, France}, pages = {1 -- 17}, publisher = {Springer Nature}, title = {{Timed alternating-time temporal logic}}, doi = {10.1007/11867340_1}, volume = {4202}, year = {2006}, } @inproceedings{4431, abstract = {We summarize some current trends in embedded systems design and point out some of their characteristics, such as the chasm between analytical and computational models, and the gap between safety-critical and best-effort engineering practices. We call for a coherent scientific foundation for embedded systems design, and we discuss a few key demands on such a foundation: the need for encompassing several manifestations of heterogeneity, and the need for constructivity in design. We believe that the development of a satisfactory Embedded Systems Design Science provides a timely challenge and opportunity for reinvigorating computer science.}, author = {Henzinger, Thomas A and Sifakis, Joseph}, booktitle = {Proceedings of the 14th international conference on Formal Methods}, isbn = {9783540372158}, issn = {1611-3349}, location = {Hamilton, Canada}, pages = {1 -- 15}, publisher = {Springer Nature}, title = {{The embedded systems design challenge}}, doi = {10.1007/11813040_1}, volume = {4085}, year = {2006}, } @inproceedings{3889, abstract = {We study observation-based strategies for two-player turn-based games on graphs with omega-regular objectives. An observation-based strategy relies on imperfect information about the history of a play, namely, on the past sequence of observations. Such games occur in the synthesis of a controller that does not see the private state of the plant. Our main results are twofold. First, we give a fixed-point algorithm for computing the set of states from which a player can win with a deterministic observation-based strategy for any omega-regular objective. The fixed point is computed in the lattice of antichains of state sets. This algorithm has the advantages of being directed by the objective and of avoiding an explicit subset construction on the game graph. Second, we give an algorithm for computing the set of states from which a player can win with probability 1 with a randomized observation-based strategy for a Buchi objective. This set is of interest because in the absence of perfect information, randomized strategies are more powerful than deterministic ones. We show that our algorithms are optimal by proving matching lower bounds.}, author = {Chatterjee, Krishnendu and Doyen, Laurent and Henzinger, Thomas A and Raskin, Jean}, booktitle = {Proceedings of the 20th international conference on Computer Science Logic}, isbn = {9783540454588}, issn = {1611-3349}, location = {Szeged, Hungary}, pages = {287 -- 302}, publisher = {Springer Nature}, title = {{Algorithms for omega-regular games with imperfect information}}, doi = {10.1007/11874683_19}, volume = {4207}, year = {2006}, } @inproceedings{3679, abstract = {This paper describes a new system for "Finding Satellite Tracks” in astronomical images based on the modern geometric approach. There is an increasing need of using methods with solid mathematical and statistical foundation in astronomical image processing. Where the computational methods are serving in all disciplines of science, they are becoming popular in the field of astronomy as well. Currently different computational systems are required to be numerically optimized before to get applied on astronomical images. So at present there is no single system which solves the problems of astronomers using computational methods based on modern approaches. The system "Finding Satellite Tracks” is based on geometric matching method "Recognition by Adaptive Subdivision of Transformation Space (RAST)".}, author = {Ali, Haider and Lampert, Christoph and Breuel, Thomas}, booktitle = {Proceedings of the 11th Iberoamerican conference on Progress in Pattern Recognition, Image Analysis and Applications}, isbn = {9783540465560}, issn = {1611-3349}, location = {Cancún, Mexico}, pages = {892 -- 901}, publisher = {Springer Nature}, title = {{Satellite tracks removal in astronomical images}}, doi = {10.1007/11892755_92}, volume = {4225}, year = {2006}, }