[{"month":"10","abstract":[{"text":"We study games played on graphs with omega-regular conditions specified as parity, Rabin, Streett or Muller conditions. These games have applications in the verification, synthesis, modeling, testing, and compatibility checking of reactive systems. Important distinctions between graph games are as follows: (a) turn-based vs. concurrent games, depending on whether at a state of the game only a single player makes a move, or players make moves simultaneously; (b) deterministic vs. stochastic, depending on whether the transition function is a deterministic or a probabilistic function over successor states; and (c) zero-sum vs. non-zero-sum, depending on whether the objectives of the players are strictly conflicting or not.\n\nWe establish that the decision problem for turn-based stochastic zero-sum games with Rabin, Streett, and Muller objectives are NP-complete, coNP-complete, and PSPACE-complete, respectively, substantially improving the previously known 3EXPTIME bound. We also present strategy improvement style algorithms for turn-based stochastic Rabin and Streett games. In the case of concurrent stochastic zero-sum games with parity objectives we obtain a PSPACE bound, again improving the previously known 3EXPTIME bound. As a consequence, concurrent stochastic zero-sum games with Rabin, Streett, and Muller objectives can be solved in EXPSPACE, improving the previously known 4EXPTIME bound. We also present an elementary and combinatorial proof of the existence of memoryless \\epsilon-optimal strategies in concurrent stochastic games with reachability objectives, for all real \\epsilon>0, where an \\epsilon-optimal strategy achieves the value of the game with in \\epsilon against all strategies of the opponent. We also use the proof techniques to present a strategy improvement style algorithm for concurrent stochastic reachability games.\n\nWe then go beyond \\omega-regular objectives and study the complexity of an important class of quantitative objectives, namely, limit-average objectives. In the case of limit-average games, the states of the graph is labeled with rewards and the goal is to maximize the long-run average of the rewards. We show that concurrent stochastic zero-sum games with limit-average objectives can be solved in EXPTIME.\n\nFinally, we introduce a new notion of equilibrium, called secure equilibrium, in non-zero-sum games which captures the notion of conditional competitiveness. We prove the existence of unique maximal secure equilibrium payoff profiles in turn-based deterministic games, and present algorithms to compute such payoff profiles. We also show how the notion of secure equilibrium extends the assume-guarantee style of reasoning in the game theoretic framework.","lang":"eng"}],"status":"public","date_created":"2018-12-11T12:09:29Z","year":"2007","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Krishnendu Chatterjee","last_name":"Chatterjee"}],"day":"08","publisher":"University of California, Berkeley","type":"dissertation","publist_id":"150","main_file_link":[{"open_access":"0","url":"http://chess.eecs.berkeley.edu/pubs/462.html"}],"extern":1,"citation":{"short":"K. Chatterjee, Stochastic ω-Regular Games, University of California, Berkeley, 2007.","ieee":"K. Chatterjee, *Stochastic ω-Regular Games*. University of California, Berkeley, 2007, pp. 1–247.","mla":"Chatterjee, Krishnendu. *Stochastic ω-Regular Games*. University of California, Berkeley, 2007, pp. 1–247.","ista":"Chatterjee K. 2007. Stochastic ω-Regular Games, University of California, Berkeley,p.","ama":"Chatterjee K. *Stochastic ω-Regular Games*. University of California, Berkeley; 2007:1-247.","apa":"Chatterjee, K. (2007). *Stochastic ω-Regular Games* (pp. 1–247). University of California, Berkeley.","chicago":"Chatterjee, Krishnendu. *Stochastic ω-Regular Games*. University of California, Berkeley, 2007."},"page":"1 - 247","title":"Stochastic ω-Regular Games","_id":"4559","date_updated":"2019-08-02T12:38:33Z","acknowledgement":"Technical Report No. UCB/EECS-2007-122","quality_controlled":0,"publication_status":"published","date_published":"2007-10-08T00:00:00Z"},{"author":[{"full_name":"Chakrabarti, Arindam","last_name":"Chakrabarti","first_name":"Arindam"}],"year":"2007","status":"public","month":"12","abstract":[{"text":"Complex system design today calls for compositional design and implementation. However each component is designed with certain assumptions about the environment it is meant to operate in, and delivering certain guarantees if those assumptions are satisfied; numerous inter-component interaction errors are introduced in the manual and error-prone integration process as there is little support in design environments for machine-readably representing these assumptions and guarantees and automatically checking consistency during integration.\n\nBased on Interface Automata we propose a framework for compositional design and analysis of systems: a set of domain-specific automata-theoretic type systems for compositional system specification and analysis by behavioral specification of open systems. We focus on three different domains: component-based hardware systems communicating on bidirectional wires. concurrent distributed recursive message-passing software systems, and embedded software system components operating in resource-constrained environments. For these domains we present approaches to formally represent the assumptions and conditional guarantees between interacting open system components. Composition of such components produces new components with the appropriate assumptions and guarantees. We check satisfaction of temporal logic specifications by such components, and the substitutability of one component with another in an arbitrary context. Using this framework one can analyze large systems incrementally without needing extensive summary information to close the system at each stage. Furthermore, we focus only on the inter-component interaction behavior without dealing with the full implementation details of each component. Many of the merits of automata-theoretic model-checking are combined with the compositionality afforded by type-system based techniques. We also present an integer-based extension of the conventional boolean verification framework motivated by our interface formalism for embedded software components.\n\nOur algorithms for checking the behavioral compatibility of component interfaces are available in our tool Chic, which can be used as a plug-in for the Java IDE JBuilder and the heterogenous modeling and design environment Ptolemy II.\n\nFinally, we address the complementary problem of partitioning a large system into meaningful coherent components by analyzing the interaction patterns between its basic elements. We demonstrate the usefulness of our partitioning approach by evaluating its efficacy in improving unit-test branch coverage for a large software system implemented in C.","lang":"eng"}],"date_created":"2018-12-11T12:09:31Z","citation":{"short":"A. Chakrabarti, A Framework for Compositional Design and Analysis of Systems, University of California, Berkeley, 2007.","ieee":"A. Chakrabarti, *A framework for compositional design and analysis of systems*. University of California, Berkeley, 2007, pp. 1–244.","mla":"Chakrabarti, Arindam. *A Framework for Compositional Design and Analysis of Systems*. University of California, Berkeley, 2007, pp. 1–244.","chicago":"Chakrabarti, Arindam. *A Framework for Compositional Design and Analysis of Systems*. University of California, Berkeley, 2007.","ama":"Chakrabarti A. *A Framework for Compositional Design and Analysis of Systems*. University of California, Berkeley; 2007:1-244.","apa":"Chakrabarti, A. (2007). *A framework for compositional design and analysis of systems* (pp. 1–244). University of California, Berkeley.","ista":"Chakrabarti A. 2007. A framework for compositional design and analysis of systems, University of California, Berkeley,p."},"extern":1,"publist_id":"145","type":"dissertation","publisher":"University of California, Berkeley","day":"20","_id":"4566","date_updated":"2019-01-24T13:20:45Z","title":"A framework for compositional design and analysis of systems","page":"1 - 244","date_published":"2007-12-20T00:00:00Z","publication_status":"published","quality_controlled":0},{"title":"Métodos no lineales y sus aplicaciones en dinámicas aleatorias de poblaciones celulares","date_updated":"2019-01-24T13:18:53Z","_id":"4236","quality_controlled":0,"publication_status":"published","doi":"3810","date_published":"2004-01-01T00:00:00Z","author":[{"last_name":"De Vladar","full_name":"de Vladar,Harold Paul","first_name":"Harold"}],"year":"2004","month":"01","date_created":"2018-12-11T12:07:46Z","status":"public","publisher":"Centro de estudios avazados, IVIC","type":"dissertation","day":"01","citation":{"mla":"De Vladar, Harold. *Métodos No Lineales y Sus Aplicaciones En Dinámicas Aleatorias de Poblaciones Celulares*. Centro de estudios avazados, IVIC, 2004, doi:3810.","chicago":"De Vladar, Harold. *Métodos No Lineales y Sus Aplicaciones En Dinámicas Aleatorias de Poblaciones Celulares*. Centro de estudios avazados, IVIC, 2004. https://doi.org/3810.","apa":"De Vladar, H. (2004). *Métodos no lineales y sus aplicaciones en dinámicas aleatorias de poblaciones celulares*. Centro de estudios avazados, IVIC. https://doi.org/3810","ama":"De Vladar H. *Métodos No Lineales y Sus Aplicaciones En Dinámicas Aleatorias de Poblaciones Celulares*. Centro de estudios avazados, IVIC; 2004. doi:3810","ista":"De Vladar H. 2004. Métodos no lineales y sus aplicaciones en dinámicas aleatorias de poblaciones celulares, Centro de estudios avazados, IVIC,p.","short":"H. De Vladar, Métodos No Lineales y Sus Aplicaciones En Dinámicas Aleatorias de Poblaciones Celulares, Centro de estudios avazados, IVIC, 2004.","ieee":"H. De Vladar, *Métodos no lineales y sus aplicaciones en dinámicas aleatorias de poblaciones celulares*. Centro de estudios avazados, IVIC, 2004."},"extern":1,"publist_id":"1877"},{"quality_controlled":0,"date_published":"2004-12-01T00:00:00Z","publication_status":"published","page":"1 - 165","title":"Program verification by lazy abstraction","_id":"4424","date_updated":"2019-01-24T13:19:57Z","day":"01","type":"dissertation","publisher":"University of California, Berkeley","publist_id":"307","citation":{"mla":"Jhala, Ranjit. *Program Verification by Lazy Abstraction*. University of California, Berkeley, 2004, pp. 1–165.","ista":"Jhala R. 2004. Program verification by lazy abstraction, University of California, Berkeley,p.","ama":"Jhala R. *Program Verification by Lazy Abstraction*. University of California, Berkeley; 2004:1-165.","apa":"Jhala, R. (2004). *Program verification by lazy abstraction* (pp. 1–165). University of California, Berkeley.","chicago":"Jhala, Ranjit. *Program Verification by Lazy Abstraction*. University of California, Berkeley, 2004.","short":"R. Jhala, Program Verification by Lazy Abstraction, University of California, Berkeley, 2004.","ieee":"R. Jhala, *Program verification by lazy abstraction*. University of California, Berkeley, 2004, pp. 1–165."},"extern":1,"year":"2004","month":"12","status":"public","abstract":[{"lang":"eng","text":"The enormous cost and ubiquity of software errors necessitates the need for techniques and tools that can precisely analyze large systems and prove that they meet given specifications, or if they don't, return counterexample behaviors showing how the system fails. Recent advances in model checking, decision procedures, program analysis and type systems, and a shift of focus to partial specifications common to several systems (e.g., memory safety and race freedom) have resulted in several practical verification methods. However, these methods are either precise or they are scalable, depending on whether they track the values of variables or only a fixed small set of dataflow facts (e.g., types), and are usually insufficient for precisely verifying large programs.\n\nWe describe a new technique called Lazy Abstraction (LA) which achieves both precision and scalability by localizing the use of precise information. LA automatically builds, explores and refines a single abstract model of the program in a way that different parts of the model exhibit different degrees of precision, namely just enough to verify the desired property. The algorithm automatically mines the information required by partitioning mechanical proofs of unsatisfiability of spurious counterexamples into Craig Interpolants. For multithreaded systems, we give a new technique based on analyzing the behavior of a single thread executing in a context which is an abstraction of the other (arbitrarily many) threads. We define novel context models and show how to automatically infer them and analyze the full system (thread + context) using LA.\n\nLA is implemented in BLAST. We have run BLAST on Windows and Linux Device Drivers to verify API conformance properties, and have used it to find (or guarantee the absence of) data races in multithreaded Networked Embedded Systems (NESC) applications. BLAST is able to prove the absence of races in several cases where earlier methods, which depend on lock-based synchronization, fail."}],"date_created":"2018-12-11T12:08:47Z","author":[{"first_name":"Ranjit","last_name":"Jhala","full_name":"Jhala, Ranjit"}]},{"publist_id":"305","extern":1,"citation":{"mla":"Horowitz, Benjamin. *Giotto: A Time-Triggered Language for Embedded Programming*. University of California, Berkeley, 2003, pp. 1–237.","apa":"Horowitz, B. (2003). *Giotto: A time-triggered language for embedded programming* (pp. 1–237). University of California, Berkeley.","ama":"Horowitz B. *Giotto: A Time-Triggered Language for Embedded Programming*. University of California, Berkeley; 2003:1-237.","ista":"Horowitz B. 2003. Giotto: A time-triggered language for embedded programming, University of California, Berkeley,p.","chicago":"Horowitz, Benjamin. *Giotto: A Time-Triggered Language for Embedded Programming*. University of California, Berkeley, 2003.","short":"B. Horowitz, Giotto: A Time-Triggered Language for Embedded Programming, University of California, Berkeley, 2003.","ieee":"B. Horowitz, *Giotto: A time-triggered language for embedded programming*. University of California, Berkeley, 2003, pp. 1–237."},"day":"01","type":"dissertation","publisher":"University of California, Berkeley","abstract":[{"text":"Giotto provides a time-triggered programmer’s model for the implementation of embedded control systems with hard real-time constraints. Giotto’s precise semantics and predictabil- ity make it suitable for safety-critical applications.\nGiotto is based around the idea that time-triggered task invocation together with time-triggered mode switching can form a useful programming model for real-time systems. To substantiate this claim, we describe the use of Giotto to refactor the software of a small, autonomous helicopter. The ease with which Giotto expresses the existing software provides evidence that Giotto is an appropriate programming language for control systems.\nSince Giotto is a real-time programming language, ensuring that Giotto programs meet their deadlines is crucial. To study precedence-constrained Giotto scheduling, we first examine single-mode, single-processor scheduling. We extend to an infinite, periodic setting the classical problem of meeting deadlines for a set of tasks with release times, deadlines, precedence constraints, and preemption. We then develop an algorithm for scheduling Giotto programs on a single processor by representing Giotto programs as instances of the extended scheduling problem.\nNext, we study multi-mode, single-processor Giotto scheduling. This problem is different from classical scheduling problems, since in our precedence-constrained approach, the deadlines of tasks may vary depending on the mode switching behavior of the program. We present conditional scheduling models which capture this varying-deadline behavior. We develop polynomial-time algorithms for some conditional scheduling models, and prove oth- ers to be computationally hard. We show how to represent multi-mode Giotto programs as instances of the model, resulting in an algorithm for scheduling multi-mode Giotto programs on a single processor.\nFinally, we show that the problem of scheduling Giotto programs for multiple net- worked processors is strongly NP-hard.","lang":"eng"}],"status":"public","month":"10","date_created":"2018-12-11T12:08:47Z","year":"2003","author":[{"first_name":"Benjamin","full_name":"Horowitz, Benjamin","last_name":"Horowitz"}],"publication_status":"published","date_published":"2003-10-01T00:00:00Z","quality_controlled":0,"date_updated":"2019-01-24T13:19:57Z","_id":"4425","page":"1 - 237","title":"Giotto: A time-triggered language for embedded programming"}]