--- _id: '3846' abstract: - lang: eng text: We summarize classical and recent results about two-player games played on graphs with ω-regular objectives. These games have applications in the verification and synthesis of reactive systems. Important distinctions are whether a graph game is turn-based or concurrent; deterministic or stochastic; zero-sum or not. We cluster known results and open problems according to these classifications. acknowledgement: This research was supported in part by the ONR grant N00014-02-1-0671, by the AFOSR MURI grant F49620-00-1-0327, and by the NSF grants CCR-9988172, CCR-0085949, and CCR-0225610. article_processing_charge: No article_type: original author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 citation: ama: Chatterjee K, Henzinger TA. A survey of stochastic ω regular games. Journal of Computer and System Sciences. 2012;78(2):394-413. doi:10.1016/j.jcss.2011.05.002 apa: Chatterjee, K., & Henzinger, T. A. (2012). A survey of stochastic ω regular games. Journal of Computer and System Sciences. Elsevier. https://doi.org/10.1016/j.jcss.2011.05.002 chicago: Chatterjee, Krishnendu, and Thomas A Henzinger. “A Survey of Stochastic ω Regular Games.” Journal of Computer and System Sciences. Elsevier, 2012. https://doi.org/10.1016/j.jcss.2011.05.002. ieee: K. Chatterjee and T. A. Henzinger, “A survey of stochastic ω regular games,” Journal of Computer and System Sciences, vol. 78, no. 2. Elsevier, pp. 394–413, 2012. ista: Chatterjee K, Henzinger TA. 2012. A survey of stochastic ω regular games. Journal of Computer and System Sciences. 78(2), 394–413. mla: Chatterjee, Krishnendu, and Thomas A. Henzinger. “A Survey of Stochastic ω Regular Games.” Journal of Computer and System Sciences, vol. 78, no. 2, Elsevier, 2012, pp. 394–413, doi:10.1016/j.jcss.2011.05.002. short: K. Chatterjee, T.A. Henzinger, Journal of Computer and System Sciences 78 (2012) 394–413. date_created: 2018-12-11T12:05:29Z date_published: 2012-03-02T00:00:00Z date_updated: 2022-05-24T08:00:54Z day: '02' ddc: - '000' department: - _id: KrCh - _id: ToHe doi: 10.1016/j.jcss.2011.05.002 file: - access_level: open_access checksum: 241b939deb4517cdd4426d49c67e3fa2 content_type: application/pdf creator: kschuh date_created: 2019-01-29T10:54:28Z date_updated: 2020-07-14T12:46:17Z file_id: '5897' file_name: a_survey_of_stochastic_omega-regular_games.pdf file_size: 336450 relation: main_file file_date_updated: 2020-07-14T12:46:17Z has_accepted_license: '1' intvolume: ' 78' issue: '2' language: - iso: eng main_file_link: - open_access: '1' url: https://doi.org/10.1016/j.jcss.2011.05.002 month: '03' oa: 1 oa_version: Submitted Version page: 394 - 413 publication: Journal of Computer and System Sciences publication_status: published publisher: Elsevier publist_id: '2341' quality_controlled: '1' scopus_import: '1' status: public title: A survey of stochastic ω regular games type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 78 year: '2012' ... --- _id: '3128' abstract: - lang: eng text: 'We consider two-player zero-sum stochastic games on graphs with ω-regular winning conditions specified as parity objectives. These games have applications in the design and control of reactive systems. We survey the complexity results for the problem of deciding the winner in such games, and in classes of interest obtained as special cases, based on the information and the power of randomization available to the players, on the class of objectives and on the winning mode. On the basis of information, these games can be classified as follows: (a) partial-observation (both players have partial view of the game); (b) one-sided partial-observation (one player has partial-observation and the other player has complete-observation); and (c) complete-observation (both players have complete view of the game). The one-sided partial-observation games have two important subclasses: the one-player games, known as partial-observation Markov decision processes (POMDPs), and the blind one-player games, known as probabilistic automata. On the basis of randomization, (a) the players may not be allowed to use randomization (pure strategies), or (b) they may choose a probability distribution over actions but the actual random choice is external and not visible to the player (actions invisible), or (c) they may use full randomization. Finally, various classes of games are obtained by restricting the parity objective to a reachability, safety, Büchi, or coBüchi condition. We also consider several winning modes, such as sure-winning (i.e., all outcomes of a strategy have to satisfy the winning condition), almost-sure winning (i.e., winning with probability 1), limit-sure winning (i.e., winning with probability arbitrarily close to 1), and value-threshold winning (i.e., winning with probability at least ν, where ν is a given rational). ' acknowledgement: 'The research was supported by Austrian Science Fund (FWF) Grant No. P 23499-N23 on Modern Graph Algorithmic Techniques in Formal Verification, FWF NFN Grant No. S11407-N23(RiSE), ERC Start grant (279307: Graph Games), Microsoft faculty fellows award, ERC Advanced grant QUAREM, and FWF Grant No. S11403-N23 (RiSE).' author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Laurent full_name: Doyen, Laurent last_name: Doyen - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 citation: ama: Chatterjee K, Doyen L, Henzinger TA. A survey of partial-observation stochastic parity games. Formal Methods in System Design. 2012;43(2):268-284. doi:10.1007/s10703-012-0164-2 apa: Chatterjee, K., Doyen, L., & Henzinger, T. A. (2012). A survey of partial-observation stochastic parity games. Formal Methods in System Design. Springer. https://doi.org/10.1007/s10703-012-0164-2 chicago: Chatterjee, Krishnendu, Laurent Doyen, and Thomas A Henzinger. “A Survey of Partial-Observation Stochastic Parity Games.” Formal Methods in System Design. Springer, 2012. https://doi.org/10.1007/s10703-012-0164-2. ieee: K. Chatterjee, L. Doyen, and T. A. Henzinger, “A survey of partial-observation stochastic parity games,” Formal Methods in System Design, vol. 43, no. 2. Springer, pp. 268–284, 2012. ista: Chatterjee K, Doyen L, Henzinger TA. 2012. A survey of partial-observation stochastic parity games. Formal Methods in System Design. 43(2), 268–284. mla: Chatterjee, Krishnendu, et al. “A Survey of Partial-Observation Stochastic Parity Games.” Formal Methods in System Design, vol. 43, no. 2, Springer, 2012, pp. 268–84, doi:10.1007/s10703-012-0164-2. short: K. Chatterjee, L. Doyen, T.A. Henzinger, Formal Methods in System Design 43 (2012) 268–284. date_created: 2018-12-11T12:01:33Z date_published: 2012-10-01T00:00:00Z date_updated: 2021-01-12T07:41:15Z day: '01' ddc: - '005' department: - _id: KrCh - _id: ToHe doi: 10.1007/s10703-012-0164-2 ec_funded: 1 file: - access_level: open_access checksum: dd3d590f383bb2ac6cfda1489ac1c42a content_type: application/pdf creator: system date_created: 2018-12-12T10:11:27Z date_updated: 2020-07-14T12:46:00Z file_id: '4882' file_name: IST-2014-303-v1+1_Survey_Partial-Observation_Stochastic_Parity_Games.pdf file_size: 163983 relation: main_file file_date_updated: 2020-07-14T12:46:00Z has_accepted_license: '1' intvolume: ' 43' issue: '2' language: - iso: eng month: '10' oa: 1 oa_version: Submitted Version page: 268 - 284 project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship publication: Formal Methods in System Design publication_status: published publisher: Springer publist_id: '3570' pubrep_id: '303' quality_controlled: '1' scopus_import: 1 status: public title: A survey of partial-observation stochastic parity games type: journal_article user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 volume: 43 year: '2012' ... --- _id: '3155' abstract: - lang: eng text: 'We propose synchronous interfaces, a new interface theory for discrete-time systems. We use an application to time-triggered scheduling to drive the design choices for our formalism; in particular, additionally to deriving useful mathematical properties, we focus on providing a syntax which is adapted to natural high-level system modeling. As a result, we develop an interface model that relies on a guarded-command based language and is equipped with shared variables and explicit discrete-time clocks. We define all standard interface operations: compatibility checking, composition, refinement, and shared refinement. Apart from the synchronous interface model, the contribution of this paper is the establishment of a formal relation between interface theories and real-time scheduling, where we demonstrate a fully automatic framework for the incremental computation of time-triggered schedules.' acknowledgement: Research partially supported by the Danish-Chinese Center for Cyber Physical Systems (Grant No.61061130541) and VKR Center of Excellence MT-LAB. alternative_title: - LNCS author: - first_name: Benoît full_name: Delahaye, Benoît last_name: Delahaye - first_name: Uli full_name: Fahrenberg, Uli last_name: Fahrenberg - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Axel full_name: Legay, Axel last_name: Legay - first_name: Dejan full_name: Nickovic, Dejan id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87 last_name: Nickovic citation: ama: 'Delahaye B, Fahrenberg U, Henzinger TA, Legay A, Nickovic D. Synchronous interface theories and time triggered scheduling. In: Vol 7273. Springer; 2012:203-218. doi:10.1007/978-3-642-30793-5_13' apa: 'Delahaye, B., Fahrenberg, U., Henzinger, T. A., Legay, A., & Nickovic, D. (2012). Synchronous interface theories and time triggered scheduling (Vol. 7273, pp. 203–218). Presented at the FORTE: Formal Techniques for Networked and Distributed Systems & FMOODS: Formal Methods for Open Object-Based Distributed Systems , Stockholm, Sweden: Springer. https://doi.org/10.1007/978-3-642-30793-5_13' chicago: Delahaye, Benoît, Uli Fahrenberg, Thomas A Henzinger, Axel Legay, and Dejan Nickovic. “Synchronous Interface Theories and Time Triggered Scheduling,” 7273:203–18. Springer, 2012. https://doi.org/10.1007/978-3-642-30793-5_13. ieee: 'B. Delahaye, U. Fahrenberg, T. A. Henzinger, A. Legay, and D. Nickovic, “Synchronous interface theories and time triggered scheduling,” presented at the FORTE: Formal Techniques for Networked and Distributed Systems & FMOODS: Formal Methods for Open Object-Based Distributed Systems , Stockholm, Sweden, 2012, vol. 7273, pp. 203–218.' ista: 'Delahaye B, Fahrenberg U, Henzinger TA, Legay A, Nickovic D. 2012. Synchronous interface theories and time triggered scheduling. FORTE: Formal Techniques for Networked and Distributed Systems & FMOODS: Formal Methods for Open Object-Based Distributed Systems , LNCS, vol. 7273, 203–218.' mla: Delahaye, Benoît, et al. Synchronous Interface Theories and Time Triggered Scheduling. Vol. 7273, Springer, 2012, pp. 203–18, doi:10.1007/978-3-642-30793-5_13. short: B. Delahaye, U. Fahrenberg, T.A. Henzinger, A. Legay, D. Nickovic, in:, Springer, 2012, pp. 203–218. conference: end_date: 2012-06-16 location: Stockholm, Sweden name: 'FORTE: Formal Techniques for Networked and Distributed Systems & FMOODS: Formal Methods for Open Object-Based Distributed Systems ' start_date: 2012-06-13 date_created: 2018-12-11T12:01:43Z date_published: 2012-06-01T00:00:00Z date_updated: 2021-01-12T07:41:26Z day: '01' ddc: - '004' department: - _id: ToHe doi: 10.1007/978-3-642-30793-5_13 file: - access_level: open_access checksum: feae2e07f2d9a59843f8ddabf25d179f content_type: application/pdf creator: system date_created: 2018-12-12T10:11:25Z date_updated: 2020-07-14T12:46:01Z file_id: '4879' file_name: IST-2012-88-v1+1_Synchronous_interface_theories_and_time_triggered_scheduling.pdf file_size: 493198 relation: main_file file_date_updated: 2020-07-14T12:46:01Z has_accepted_license: '1' intvolume: ' 7273' language: - iso: eng month: '06' oa: 1 oa_version: Submitted Version page: 203 - 218 publication_status: published publisher: Springer publist_id: '3539' pubrep_id: '88' quality_controlled: '1' scopus_import: 1 status: public title: Synchronous interface theories and time triggered scheduling type: conference user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 volume: 7273 year: '2012' ... --- _id: '3836' abstract: - lang: eng text: Hierarchical Timing Language (HTL) is a coordination language for distributed, hard real-time applications. HTL is a hierarchical extension of Giotto and, like its predecessor, based on the logical execution time (LET) paradigm of real-time programming. Giotto is compiled into code for a virtual machine, called the EmbeddedMachine (or E machine). If HTL is targeted to the E machine, then the hierarchicalprogram structure needs to be flattened; the flattening makes separatecompilation difficult, and may result in E machinecode of exponential size. In this paper, we propose a generalization of the E machine, which supports a hierarchicalprogram structure at runtime through real-time trigger mechanisms that are arranged in a tree. We present the generalized E machine, and a modular compiler for HTL that generates code of linear size. The compiler may generate code for any part of a given HTL program separately in any order. author: - first_name: Arkadeb full_name: Ghosal, Arkadeb last_name: Ghosal - first_name: Daniel full_name: Iercan, Daniel last_name: Iercan - first_name: Christoph full_name: Kirsch, Christoph last_name: Kirsch - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Alberto full_name: Sangiovanni Vincentelli, Alberto last_name: Sangiovanni Vincentelli citation: ama: Ghosal A, Iercan D, Kirsch C, Henzinger TA, Sangiovanni Vincentelli A. Separate compilation of hierarchical real-time programs into linear-bounded embedded machine code. Science of Computer Programming. 2012;77(2):96-112. doi:10.1016/j.scico.2010.06.004 apa: Ghosal, A., Iercan, D., Kirsch, C., Henzinger, T. A., & Sangiovanni Vincentelli, A. (2012). Separate compilation of hierarchical real-time programs into linear-bounded embedded machine code. Science of Computer Programming. Elsevier. https://doi.org/10.1016/j.scico.2010.06.004 chicago: Ghosal, Arkadeb, Daniel Iercan, Christoph Kirsch, Thomas A Henzinger, and Alberto Sangiovanni Vincentelli. “Separate Compilation of Hierarchical Real-Time Programs into Linear-Bounded Embedded Machine Code.” Science of Computer Programming. Elsevier, 2012. https://doi.org/10.1016/j.scico.2010.06.004. ieee: A. Ghosal, D. Iercan, C. Kirsch, T. A. Henzinger, and A. Sangiovanni Vincentelli, “Separate compilation of hierarchical real-time programs into linear-bounded embedded machine code,” Science of Computer Programming, vol. 77, no. 2. Elsevier, pp. 96–112, 2012. ista: Ghosal A, Iercan D, Kirsch C, Henzinger TA, Sangiovanni Vincentelli A. 2012. Separate compilation of hierarchical real-time programs into linear-bounded embedded machine code. Science of Computer Programming. 77(2), 96–112. mla: Ghosal, Arkadeb, et al. “Separate Compilation of Hierarchical Real-Time Programs into Linear-Bounded Embedded Machine Code.” Science of Computer Programming, vol. 77, no. 2, Elsevier, 2012, pp. 96–112, doi:10.1016/j.scico.2010.06.004. short: A. Ghosal, D. Iercan, C. Kirsch, T.A. Henzinger, A. Sangiovanni Vincentelli, Science of Computer Programming 77 (2012) 96–112. date_created: 2018-12-11T12:05:26Z date_published: 2012-02-01T00:00:00Z date_updated: 2021-01-12T07:52:32Z day: '01' department: - _id: ToHe doi: 10.1016/j.scico.2010.06.004 intvolume: ' 77' issue: '2' language: - iso: eng month: '02' oa_version: None page: 96 - 112 publication: Science of Computer Programming publication_status: published publisher: Elsevier publist_id: '2370' quality_controlled: '1' scopus_import: 1 status: public title: Separate compilation of hierarchical real-time programs into linear-bounded embedded machine code type: journal_article user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 volume: 77 year: '2012' ... --- _id: '2967' abstract: - lang: eng text: For programs whose data variables range over Boolean or finite domains, program verification is decidable, and this forms the basis of recent tools for software model checking. In this article, we consider algorithmic verification of programs that use Boolean variables, and in addition, access a single read-only array whose length is potentially unbounded, and whose elements range over an unbounded data domain. We show that the reachability problem, while undecidable in general, is (1) PSPACE-complete for programs in which the array-accessing for-loops are not nested, (2) decidable for a restricted class of programs with doubly nested loops. The second result establishes connections to automata and logics defining languages over data words. acknowledgement: This research was supported in part by the NSF Cybertrust award CNS 0524059, by the European Research Council (ERC) Advanced Investigator Grant QUAREM, and by the Austrian Science Fund (FWF) project S11402-N23. article_number: '27' author: - first_name: Rajeev full_name: Alur, Rajeev last_name: Alur - first_name: Pavol full_name: Cerny, Pavol id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87 last_name: Cerny - first_name: Scott full_name: Weinstein, Scott last_name: Weinstein citation: ama: Alur R, Cerny P, Weinstein S. Algorithmic analysis of array-accessing programs. ACM Transactions on Computational Logic (TOCL). 2012;13(3). doi:10.1145/2287718.2287727 apa: Alur, R., Cerny, P., & Weinstein, S. (2012). Algorithmic analysis of array-accessing programs. ACM Transactions on Computational Logic (TOCL). ACM. https://doi.org/10.1145/2287718.2287727 chicago: Alur, Rajeev, Pavol Cerny, and Scott Weinstein. “Algorithmic Analysis of Array-Accessing Programs.” ACM Transactions on Computational Logic (TOCL). ACM, 2012. https://doi.org/10.1145/2287718.2287727. ieee: R. Alur, P. Cerny, and S. Weinstein, “Algorithmic analysis of array-accessing programs,” ACM Transactions on Computational Logic (TOCL), vol. 13, no. 3. ACM, 2012. ista: Alur R, Cerny P, Weinstein S. 2012. Algorithmic analysis of array-accessing programs. ACM Transactions on Computational Logic (TOCL). 13(3), 27. mla: Alur, Rajeev, et al. “Algorithmic Analysis of Array-Accessing Programs.” ACM Transactions on Computational Logic (TOCL), vol. 13, no. 3, 27, ACM, 2012, doi:10.1145/2287718.2287727. short: R. Alur, P. Cerny, S. Weinstein, ACM Transactions on Computational Logic (TOCL) 13 (2012). date_created: 2018-12-11T12:00:36Z date_published: 2012-08-01T00:00:00Z date_updated: 2023-02-23T12:09:43Z day: '01' department: - _id: ToHe doi: 10.1145/2287718.2287727 ec_funded: 1 intvolume: ' 13' issue: '3' language: - iso: eng month: '08' oa_version: None project: - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering publication: ACM Transactions on Computational Logic (TOCL) publication_status: published publisher: ACM publist_id: '3748' quality_controlled: '1' related_material: record: - id: '4403' relation: earlier_version status: public scopus_import: 1 status: public title: Algorithmic analysis of array-accessing programs type: journal_article user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 volume: 13 year: '2012' ... --- _id: '494' abstract: - lang: eng text: We solve the longstanding open problems of the blow-up involved in the translations, when possible, of a nondeterministic Büchi word automaton (NBW) to a nondeterministic co-Büchi word automaton (NCW) and to a deterministic co-Büchi word automaton (DCW). For the NBW to NCW translation, the currently known upper bound is 2o(nlog n) and the lower bound is 1.5n. We improve the upper bound to n2n and describe a matching lower bound of 2ω(n). For the NBW to DCW translation, the currently known upper bound is 2o(nlog n). We improve it to 2 o(n), which is asymptotically tight. Both of our upper-bound constructions are based on a simple subset construction, do not involve intermediate automata with richer acceptance conditions, and can be implemented symbolically. We continue and solve the open problems of translating nondeterministic Streett, Rabin, Muller, and parity word automata to NCW and to DCW. Going via an intermediate NBW is not optimal and we describe direct, simple, and asymptotically tight constructions, involving a 2o(n) blow-up. The constructions are variants of the subset construction, providing a unified approach for translating all common classes of automata to NCW and DCW. Beyond the theoretical importance of the results, we point to numerous applications of the new constructions. In particular, they imply a simple subset-construction based translation, when possible, of LTL to deterministic Büchi word automata. article_number: '29' author: - first_name: Udi full_name: Boker, Udi id: 31E297B6-F248-11E8-B48F-1D18A9856A87 last_name: Boker - first_name: Orna full_name: Kupferman, Orna last_name: Kupferman citation: ama: Boker U, Kupferman O. Translating to Co-Büchi made tight, unified, and useful. ACM Transactions on Computational Logic (TOCL). 2012;13(4). doi:10.1145/2362355.2362357 apa: Boker, U., & Kupferman, O. (2012). Translating to Co-Büchi made tight, unified, and useful. ACM Transactions on Computational Logic (TOCL). ACM. https://doi.org/10.1145/2362355.2362357 chicago: Boker, Udi, and Orna Kupferman. “Translating to Co-Büchi Made Tight, Unified, and Useful.” ACM Transactions on Computational Logic (TOCL). ACM, 2012. https://doi.org/10.1145/2362355.2362357. ieee: U. Boker and O. Kupferman, “Translating to Co-Büchi made tight, unified, and useful,” ACM Transactions on Computational Logic (TOCL), vol. 13, no. 4. ACM, 2012. ista: Boker U, Kupferman O. 2012. Translating to Co-Büchi made tight, unified, and useful. ACM Transactions on Computational Logic (TOCL). 13(4), 29. mla: Boker, Udi, and Orna Kupferman. “Translating to Co-Büchi Made Tight, Unified, and Useful.” ACM Transactions on Computational Logic (TOCL), vol. 13, no. 4, 29, ACM, 2012, doi:10.1145/2362355.2362357. short: U. Boker, O. Kupferman, ACM Transactions on Computational Logic (TOCL) 13 (2012). date_created: 2018-12-11T11:46:47Z date_published: 2012-10-01T00:00:00Z date_updated: 2021-01-12T08:01:03Z day: '01' department: - _id: ToHe doi: 10.1145/2362355.2362357 intvolume: ' 13' issue: '4' language: - iso: eng month: '10' oa_version: None publication: ACM Transactions on Computational Logic (TOCL) publication_status: published publisher: ACM publist_id: '7326' quality_controlled: '1' scopus_import: 1 status: public title: Translating to Co-Büchi made tight, unified, and useful type: journal_article user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 volume: 13 year: '2012' ... --- _id: '3249' abstract: - lang: eng text: Boolean notions of correctness are formalized by preorders on systems. Quantitative measures of correctness can be formalized by real-valued distance functions between systems, where the distance between implementation and specification provides a measure of "fit" or "desirability". We extend the simulation preorder to the quantitative setting by making each player of a simulation game pay a certain price for her choices. We use the resulting games with quantitative objectives to define three different simulation distances. The correctness distance measures how much the specification must be changed in order to be satisfied by the implementation. The coverage distance measures how much the implementation restricts the degrees of freedom offered by the specification. The robustness distance measures how much a system can deviate from the implementation description without violating the specification. We consider these distances for safety as well as liveness specifications. The distances can be computed in polynomial time for safety specifications, and for liveness specifications given by weak fairness constraints. We show that the distance functions satisfy the triangle inequality, that the distance between two systems does not increase under parallel composition with a third system, and that the distance between two systems can be bounded from above and below by distances between abstractions of the two systems. These properties suggest that our simulation distances provide an appropriate basis for a quantitative theory of discrete systems. We also demonstrate how the robustness distance can be used to measure how many transmission errors are tolerated by error correcting codes. acknowledgement: This work was partially supported by the ERC Advanced Grant QUAREM, the FWF NFN Grant S11402-N23 (RiSE), the European Union project COMBEST and the European Network of Excellence Artist Design. author: - first_name: Pavol full_name: Cerny, Pavol id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87 last_name: Cerny - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Arjun full_name: Radhakrishna, Arjun id: 3B51CAC4-F248-11E8-B48F-1D18A9856A87 last_name: Radhakrishna citation: ama: Cerny P, Henzinger TA, Radhakrishna A. Simulation distances. Theoretical Computer Science. 2012;413(1):21-35. doi:10.1016/j.tcs.2011.08.002 apa: Cerny, P., Henzinger, T. A., & Radhakrishna, A. (2012). Simulation distances. Theoretical Computer Science. Elsevier. https://doi.org/10.1016/j.tcs.2011.08.002 chicago: Cerny, Pavol, Thomas A Henzinger, and Arjun Radhakrishna. “Simulation Distances.” Theoretical Computer Science. Elsevier, 2012. https://doi.org/10.1016/j.tcs.2011.08.002. ieee: P. Cerny, T. A. Henzinger, and A. Radhakrishna, “Simulation distances,” Theoretical Computer Science, vol. 413, no. 1. Elsevier, pp. 21–35, 2012. ista: Cerny P, Henzinger TA, Radhakrishna A. 2012. Simulation distances. Theoretical Computer Science. 413(1), 21–35. mla: Cerny, Pavol, et al. “Simulation Distances.” Theoretical Computer Science, vol. 413, no. 1, Elsevier, 2012, pp. 21–35, doi:10.1016/j.tcs.2011.08.002. short: P. Cerny, T.A. Henzinger, A. Radhakrishna, Theoretical Computer Science 413 (2012) 21–35. date_created: 2018-12-11T12:02:15Z date_published: 2012-01-06T00:00:00Z date_updated: 2023-02-23T12:24:04Z day: '06' department: - _id: ToHe doi: 10.1016/j.tcs.2011.08.002 ec_funded: 1 intvolume: ' 413' issue: '1' language: - iso: eng month: '01' oa_version: None page: 21 - 35 project: - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 25EFB36C-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '215543' name: COMponent-Based Embedded Systems design Techniques - _id: 25F1337C-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '214373' name: Design for Embedded Systems publication: Theoretical Computer Science publication_status: published publisher: Elsevier publist_id: '3408' pubrep_id: '42' quality_controlled: '1' related_material: record: - id: '4393' relation: earlier_version status: public - id: '5389' relation: earlier_version status: public scopus_import: 1 status: public title: Simulation distances type: journal_article user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 volume: 413 year: '2012' ... --- _id: '10903' abstract: - lang: eng text: We propose a logic-based framework for automated reasoning about sequential programs manipulating singly-linked lists and arrays with unbounded data. We introduce the logic SLAD, which allows combining shape constraints, written in a fragment of Separation Logic, with data and size constraints. We address the problem of checking the entailment between SLAD formulas, which is crucial in performing pre-post condition reasoning. Although this problem is undecidable in general for SLAD, we propose a sound and powerful procedure that is able to solve this problem for a large class of formulas, beyond the capabilities of existing techniques and tools. We prove that this procedure is complete, i.e., it is actually a decision procedure for this problem, for an important fragment of SLAD including known decidable logics. We implemented this procedure and shown its preciseness and its efficiency on a significant benchmark of formulas. acknowledgement: This work has been partially supported by the French ANR project Veridyc alternative_title: - LNCS article_processing_charge: No author: - first_name: Ahmed full_name: Bouajjani, Ahmed last_name: Bouajjani - first_name: Cezara full_name: Dragoi, Cezara id: 2B2B5ED0-F248-11E8-B48F-1D18A9856A87 last_name: Dragoi - first_name: Constantin full_name: Enea, Constantin last_name: Enea - first_name: Mihaela full_name: Sighireanu, Mihaela last_name: Sighireanu citation: ama: 'Bouajjani A, Dragoi C, Enea C, Sighireanu M. Accurate invariant checking for programs manipulating lists and arrays with infinite data. In: Automated Technology for Verification and Analysis. Vol 7561. LNCS. Berlin, Heidelberg: Springer; 2012:167-182. doi:10.1007/978-3-642-33386-6_14' apa: 'Bouajjani, A., Dragoi, C., Enea, C., & Sighireanu, M. (2012). Accurate invariant checking for programs manipulating lists and arrays with infinite data. In Automated Technology for Verification and Analysis (Vol. 7561, pp. 167–182). Berlin, Heidelberg: Springer. https://doi.org/10.1007/978-3-642-33386-6_14' chicago: 'Bouajjani, Ahmed, Cezara Dragoi, Constantin Enea, and Mihaela Sighireanu. “Accurate Invariant Checking for Programs Manipulating Lists and Arrays with Infinite Data.” In Automated Technology for Verification and Analysis, 7561:167–82. LNCS. Berlin, Heidelberg: Springer, 2012. https://doi.org/10.1007/978-3-642-33386-6_14.' ieee: A. Bouajjani, C. Dragoi, C. Enea, and M. Sighireanu, “Accurate invariant checking for programs manipulating lists and arrays with infinite data,” in Automated Technology for Verification and Analysis, Thiruvananthapuram, India, 2012, vol. 7561, pp. 167–182. ista: 'Bouajjani A, Dragoi C, Enea C, Sighireanu M. 2012. Accurate invariant checking for programs manipulating lists and arrays with infinite data. Automated Technology for Verification and Analysis. ATVA: Automated Technology for Verification and AnalysisLNCS, LNCS, vol. 7561, 167–182.' mla: Bouajjani, Ahmed, et al. “Accurate Invariant Checking for Programs Manipulating Lists and Arrays with Infinite Data.” Automated Technology for Verification and Analysis, vol. 7561, Springer, 2012, pp. 167–82, doi:10.1007/978-3-642-33386-6_14. short: A. Bouajjani, C. Dragoi, C. Enea, M. Sighireanu, in:, Automated Technology for Verification and Analysis, Springer, Berlin, Heidelberg, 2012, pp. 167–182. conference: end_date: 2012-10-06 location: Thiruvananthapuram, India name: 'ATVA: Automated Technology for Verification and Analysis' start_date: 2012-10-03 date_created: 2022-03-21T07:58:39Z date_published: 2012-10-15T00:00:00Z date_updated: 2023-09-05T14:07:24Z day: '15' department: - _id: ToHe doi: 10.1007/978-3-642-33386-6_14 intvolume: ' 7561' language: - iso: eng month: '10' oa_version: None page: 167-182 place: Berlin, Heidelberg publication: Automated Technology for Verification and Analysis publication_identifier: eisbn: - '9783642333866' eissn: - 1611-3349 isbn: - '9783642333859' issn: - 0302-9743 publication_status: published publisher: Springer quality_controlled: '1' scopus_import: '1' series_title: LNCS status: public title: Accurate invariant checking for programs manipulating lists and arrays with infinite data type: conference user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1 volume: 7561 year: '2012' ... --- _id: '10906' abstract: - lang: eng text: HSF(C) is a tool that automates verification of safety and liveness properties for C programs. This paper describes the verification approach taken by HSF(C) and provides instructions on how to install and use the tool. alternative_title: - LNCS article_processing_charge: No author: - first_name: Sergey full_name: Grebenshchikov, Sergey last_name: Grebenshchikov - first_name: Ashutosh full_name: Gupta, Ashutosh id: 335E5684-F248-11E8-B48F-1D18A9856A87 last_name: Gupta - first_name: Nuno P. full_name: Lopes, Nuno P. last_name: Lopes - first_name: Corneliu full_name: Popeea, Corneliu last_name: Popeea - first_name: Andrey full_name: Rybalchenko, Andrey last_name: Rybalchenko citation: ama: 'Grebenshchikov S, Gupta A, Lopes NP, Popeea C, Rybalchenko A. HSF(C): A software verifier based on Horn clauses. In: Flanagan C, König B, eds. Tools and Algorithms for the Construction and Analysis of Systems. Vol 7214. LNCS. Berlin, Heidelberg: Springer; 2012:549-551. doi:10.1007/978-3-642-28756-5_46' apa: 'Grebenshchikov, S., Gupta, A., Lopes, N. P., Popeea, C., & Rybalchenko, A. (2012). HSF(C): A software verifier based on Horn clauses. In C. Flanagan & B. König (Eds.), Tools and Algorithms for the Construction and Analysis of Systems (Vol. 7214, pp. 549–551). Berlin, Heidelberg: Springer. https://doi.org/10.1007/978-3-642-28756-5_46' chicago: 'Grebenshchikov, Sergey, Ashutosh Gupta, Nuno P. Lopes, Corneliu Popeea, and Andrey Rybalchenko. “HSF(C): A Software Verifier Based on Horn Clauses.” In Tools and Algorithms for the Construction and Analysis of Systems, edited by Cormac Flanagan and Barbara König, 7214:549–51. LNCS. Berlin, Heidelberg: Springer, 2012. https://doi.org/10.1007/978-3-642-28756-5_46.' ieee: 'S. Grebenshchikov, A. Gupta, N. P. Lopes, C. Popeea, and A. Rybalchenko, “HSF(C): A software verifier based on Horn clauses,” in Tools and Algorithms for the Construction and Analysis of Systems, Tallinn, Estonia, 2012, vol. 7214, pp. 549–551.' ista: 'Grebenshchikov S, Gupta A, Lopes NP, Popeea C, Rybalchenko A. 2012. HSF(C): A software verifier based on Horn clauses. Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of SystemsLNCS, LNCS, vol. 7214, 549–551.' mla: 'Grebenshchikov, Sergey, et al. “HSF(C): A Software Verifier Based on Horn Clauses.” Tools and Algorithms for the Construction and Analysis of Systems, edited by Cormac Flanagan and Barbara König, vol. 7214, Springer, 2012, pp. 549–51, doi:10.1007/978-3-642-28756-5_46.' short: S. Grebenshchikov, A. Gupta, N.P. Lopes, C. Popeea, A. Rybalchenko, in:, C. Flanagan, B. König (Eds.), Tools and Algorithms for the Construction and Analysis of Systems, Springer, Berlin, Heidelberg, 2012, pp. 549–551. conference: end_date: 2012-04-01 location: Tallinn, Estonia name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems' start_date: 2012-03-24 date_created: 2022-03-21T08:03:30Z date_published: 2012-04-01T00:00:00Z date_updated: 2023-09-05T14:09:54Z day: '01' department: - _id: ToHe doi: 10.1007/978-3-642-28756-5_46 editor: - first_name: Cormac full_name: Flanagan, Cormac last_name: Flanagan - first_name: Barbara full_name: König, Barbara last_name: König intvolume: ' 7214' language: - iso: eng main_file_link: - open_access: '1' url: https://doi.org/10.1007/978-3-642-28756-5_46 month: '04' oa: 1 oa_version: Published Version page: 549-551 place: Berlin, Heidelberg publication: Tools and Algorithms for the Construction and Analysis of Systems publication_identifier: eisbn: - '9783642287565' eissn: - 1611-3349 isbn: - '9783642287558' issn: - 0302-9743 publication_status: published publisher: Springer quality_controlled: '1' scopus_import: '1' series_title: LNCS status: public title: 'HSF(C): A software verifier based on Horn clauses' type: conference user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1 volume: 7214 year: '2012' ... --- _id: '5745' article_processing_charge: No author: - first_name: Ashutosh full_name: Gupta, Ashutosh last_name: Gupta citation: ama: 'Gupta A. Improved Single Pass Algorithms for Resolution Proof Reduction. In: Automated Technology for Verification and Analysis. Vol 7561. LNCS. Berlin, Heidelberg: Springer Berlin Heidelberg; 2012:107-121. doi:10.1007/978-3-642-33386-6_10' apa: 'Gupta, A. (2012). Improved Single Pass Algorithms for Resolution Proof Reduction. In Automated Technology for Verification and Analysis (Vol. 7561, pp. 107–121). Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-642-33386-6_10' chicago: 'Gupta, Ashutosh. “Improved Single Pass Algorithms for Resolution Proof Reduction.” In Automated Technology for Verification and Analysis, 7561:107–21. LNCS. Berlin, Heidelberg: Springer Berlin Heidelberg, 2012. https://doi.org/10.1007/978-3-642-33386-6_10.' ieee: 'A. Gupta, “Improved Single Pass Algorithms for Resolution Proof Reduction,” in Automated Technology for Verification and Analysis, vol. 7561, Berlin, Heidelberg: Springer Berlin Heidelberg, 2012, pp. 107–121.' ista: 'Gupta A. 2012.Improved Single Pass Algorithms for Resolution Proof Reduction. In: Automated Technology for Verification and Analysis. vol. 7561, 107–121.' mla: Gupta, Ashutosh. “Improved Single Pass Algorithms for Resolution Proof Reduction.” Automated Technology for Verification and Analysis, vol. 7561, Springer Berlin Heidelberg, 2012, pp. 107–21, doi:10.1007/978-3-642-33386-6_10. short: A. Gupta, in:, Automated Technology for Verification and Analysis, Springer Berlin Heidelberg, Berlin, Heidelberg, 2012, pp. 107–121. conference: end_date: 2012-10-06 location: Thiruvananthapuram, Kerala, India name: ATVA 2012 start_date: 2012-10-03 date_created: 2018-12-18T13:01:46Z date_published: 2012-01-01T00:00:00Z date_updated: 2023-09-05T14:15:29Z ddc: - '005' department: - _id: ToHe doi: 10.1007/978-3-642-33386-6_10 ec_funded: 1 file: - access_level: open_access checksum: 68415837a315de3cc4d120f6019d752c content_type: application/pdf creator: dernst date_created: 2018-12-18T13:07:35Z date_updated: 2020-07-14T12:47:10Z file_id: '5746' file_name: 2012_ATVA_Gupta.pdf file_size: 465502 relation: main_file file_date_updated: 2020-07-14T12:47:10Z has_accepted_license: '1' intvolume: ' 7561' language: - iso: eng oa: 1 oa_version: None page: 107-121 place: Berlin, Heidelberg project: - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling publication: Automated Technology for Verification and Analysis publication_identifier: eissn: - 1611-3349 isbn: - '9783642333859' - '9783642333866' issn: - 0302-9743 publication_status: published publisher: Springer Berlin Heidelberg pubrep_id: '180' quality_controlled: '1' series_title: LNCS status: public title: Improved Single Pass Algorithms for Resolution Proof Reduction type: book_chapter user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1 volume: 7561 year: '2012' ...