[{"date_published":"2001-08-13T00:00:00Z","_id":"4632","abstract":[{"lang":"eng","text":"We present a compositional trace-based model for probabilistic systems. The behavior of a system with probabilistic choice is a stochastic process, namely, a probability distribution on traces, or “bundle.” Consequently, the semantics of a system with both nondeterministic and probabilistic choice is a set of bundles. The bundles of a composite system can be obtained by combining the bundles of the components in a simple mathematical way. Refinement between systems is bundle containment. We achieve assume-guarantee compositionality for bundle semantics by introducing two scoping mechanisms. The first mechanism, which is standard in compositional modeling, distinguishes inputs from outputs and hidden state. The second mechanism, which arises in probabilistic systems, partitions the state into probabilistically independent regions."}],"article_processing_charge":"No","volume":2154,"publication_status":"published","year":"2001","oa_version":"None","publist_id":"75","publication_identifier":{"isbn":["9783540424970"]},"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","date_updated":"2023-05-08T10:24:59Z","scopus_import":"1","date_created":"2018-12-11T12:09:51Z","extern":"1","month":"08","page":"351 - 365","intvolume":"      2154","status":"public","quality_controlled":"1","publication":"Proceedings of the 12th International Conference on on Concurrency Theory","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","alternative_title":["LNCS"],"type":"conference","author":[{"last_name":"De Alfaro","full_name":"De Alfaro, Luca","first_name":"Luca"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"first_name":"Ranjit","full_name":"Jhala, Ranjit","last_name":"Jhala"}],"day":"13","conference":{"name":"CONCUR: Concurrency Theory","start_date":"2001-08-20","end_date":"2001-08-25","location":"Aalborg, Denmark"},"title":"Compositional methods for probabilistic systems","citation":{"mla":"De Alfaro, Luca, et al. “Compositional Methods for Probabilistic Systems.” <i>Proceedings of the 12th International Conference on on Concurrency Theory</i>, vol. 2154, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2001, pp. 351–65, doi:<a href=\"https://doi.org/10.1007/3-540-44685-0_24\">10.1007/3-540-44685-0_24</a>.","ista":"De Alfaro L, Henzinger TA, Jhala R. 2001. Compositional methods for probabilistic systems. Proceedings of the 12th International Conference on on Concurrency Theory. CONCUR: Concurrency Theory, LNCS, vol. 2154, 351–365.","ieee":"L. De Alfaro, T. A. Henzinger, and R. Jhala, “Compositional methods for probabilistic systems,” in <i>Proceedings of the 12th International Conference on on Concurrency Theory</i>, Aalborg, Denmark, 2001, vol. 2154, pp. 351–365.","chicago":"De Alfaro, Luca, Thomas A Henzinger, and Ranjit Jhala. “Compositional Methods for Probabilistic Systems.” In <i>Proceedings of the 12th International Conference on on Concurrency Theory</i>, 2154:351–65. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2001. <a href=\"https://doi.org/10.1007/3-540-44685-0_24\">https://doi.org/10.1007/3-540-44685-0_24</a>.","apa":"De Alfaro, L., Henzinger, T. A., &#38; Jhala, R. (2001). Compositional methods for probabilistic systems. In <i>Proceedings of the 12th International Conference on on Concurrency Theory</i> (Vol. 2154, pp. 351–365). Aalborg, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.1007/3-540-44685-0_24\">https://doi.org/10.1007/3-540-44685-0_24</a>","ama":"De Alfaro L, Henzinger TA, Jhala R. Compositional methods for probabilistic systems. In: <i>Proceedings of the 12th International Conference on on Concurrency Theory</i>. Vol 2154. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2001:351-365. doi:<a href=\"https://doi.org/10.1007/3-540-44685-0_24\">10.1007/3-540-44685-0_24</a>","short":"L. De Alfaro, T.A. Henzinger, R. Jhala, in:, Proceedings of the 12th International Conference on on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2001, pp. 351–365."},"doi":"10.1007/3-540-44685-0_24","language":[{"iso":"eng"}],"acknowledgement":"This research was supported in part by the SRC contract 99-TJ-683.003, the AFOSR MURI grant F49620-00-1-0327, the MARCO GSRC grant 98-DT-660, the NSF Theory grant CCR-9988172, and the DARPA SEC grant F33615-C-98-3614."},{"publist_id":"73","oa_version":"None","year":"2001","scopus_import":"1","date_updated":"2023-05-08T09:57:31Z","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publication_identifier":{"isbn":["9783540424970"]},"article_processing_charge":"No","_id":"4633","date_published":"2001-08-13T00:00:00Z","abstract":[{"text":"A procedure for the analysis of state spaces is called symbolic if it manipulates not individual states, but sets of states that are represented by constraints. Such a procedure can be used for the analysis of infinite state spaces, provided termination is guaranteed. We present symbolic procedures, and corresponding termination criteria, for the solution of infinite-state games, which occur in the control and modular verification of infinite-state systems. To characterize the termination of symbolic procedures for solving infinite-state games, we classify these game structures into four increasingly restrictive categories:\r\n1  \tClass 1 consists of infinite-state structures for which all safety and reachability games can be solved.\r\n2  \tClass 2 consists of infinite-state structures for which all ω-regular games can be solved.\r\n3  \tClass 3 consists of infinite-state structures for which all nested positive boolean combinations of ω-regular games can be solved.\r\n4  \tClass 4 consists of infinite-state structures for which all nested boolean combinations of ω-regular games can be solved.\r\nWe give a structural characterization for each class, using equivalence relations on the state spaces of games which range from game versions of trace equivalence to a game version of bisimilarity. We provide infinite-state examples for all four classes of games from control problems for hybrid systems. We conclude by presenting symbolic algorithms for the synthesis of winning strategies (“controller synthesis”) for infinitestate games with arbitrary ω-regular objectives, and prove termination over all class-2 structures. This settles, in particular, the symbolic controller synthesis problem for rectangular hybrid systems.","lang":"eng"}],"publication_status":"published","volume":2154,"citation":{"ieee":"L. De Alfaro, T. A. Henzinger, and R. Majumdar, “Symbolic algorithms for infinite-state games,” in <i>Proceedings of the 12th International Conference on on Concurrency Theory</i>, Aalborg, Denmark, 2001, vol. 2154, pp. 536–550.","ista":"De Alfaro L, Henzinger TA, Majumdar R. 2001. Symbolic algorithms for infinite-state games. Proceedings of the 12th International Conference on on Concurrency Theory. CONCUR: Concurrency Theory, LNCS, vol. 2154, 536–550.","chicago":"De Alfaro, Luca, Thomas A Henzinger, and Ritankar Majumdar. “Symbolic Algorithms for Infinite-State Games.” In <i>Proceedings of the 12th International Conference on on Concurrency Theory</i>, 2154:536–50. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2001. <a href=\"https://doi.org/10.1007/3-540-44685-0_36\">https://doi.org/10.1007/3-540-44685-0_36</a>.","mla":"De Alfaro, Luca, et al. “Symbolic Algorithms for Infinite-State Games.” <i>Proceedings of the 12th International Conference on on Concurrency Theory</i>, vol. 2154, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2001, pp. 536–50, doi:<a href=\"https://doi.org/10.1007/3-540-44685-0_36\">10.1007/3-540-44685-0_36</a>.","short":"L. De Alfaro, T.A. Henzinger, R. Majumdar, in:, Proceedings of the 12th International Conference on on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2001, pp. 536–550.","apa":"De Alfaro, L., Henzinger, T. A., &#38; Majumdar, R. (2001). Symbolic algorithms for infinite-state games. In <i>Proceedings of the 12th International Conference on on Concurrency Theory</i> (Vol. 2154, pp. 536–550). Aalborg, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.1007/3-540-44685-0_36\">https://doi.org/10.1007/3-540-44685-0_36</a>","ama":"De Alfaro L, Henzinger TA, Majumdar R. Symbolic algorithms for infinite-state games. In: <i>Proceedings of the 12th International Conference on on Concurrency Theory</i>. Vol 2154. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2001:536-550. doi:<a href=\"https://doi.org/10.1007/3-540-44685-0_36\">10.1007/3-540-44685-0_36</a>"},"title":"Symbolic algorithms for infinite-state games","conference":{"location":"Aalborg, Denmark","start_date":"2001-08-20","end_date":"2001-08-25","name":"CONCUR: Concurrency Theory"},"day":"13","type":"conference","author":[{"first_name":"Luca","full_name":"De Alfaro, Luca","last_name":"De Alfaro"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"last_name":"Majumdar","first_name":"Ritankar","full_name":"Majumdar, Ritankar"}],"alternative_title":["LNCS"],"acknowledgement":"This research was supported in part by the AFOSR MURI grant F49620-00-1-0327, the DARPA SEC grant F33615-C-98-3614, the MARCO GSRC grant 98-DT-660, the NSF Theory grant CCR-9988172, and the NSF ITR grant CCR-0085949.","language":[{"iso":"eng"}],"doi":"10.1007/3-540-44685-0_36","page":"536 - 550","month":"08","extern":"1","date_created":"2018-12-11T12:09:52Z","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","publication":"Proceedings of the 12th International Conference on on Concurrency Theory","quality_controlled":"1","status":"public","intvolume":"      2154"},{"volume":2154,"publication_status":"published","date_published":"2001-08-13T00:00:00Z","_id":"4634","abstract":[{"lang":"eng","text":"A controller is an environment for a system that achieves a particular control objective by providing inputs to the system without constraining the choices of the system. For synchronous systems, where system and controller make simultaneous and interdependent choices, the notion that a controller must not constrain the choices of the system can be formalized by type systems for composability. In a previous paper, we solved the control problem for static and dynamic types: a static type is a dependency relation between inputs and outputs, and composition is well-typed if it does not introduce cyclic dependencies; a dynamic type is a set of static types, one for each state. Static and dynamic types, however, cannot capture many important digital circuits, such as gated clocks, bidirectional buses, and random-access memory. We therefore introduce more general type systems, so-called dependent and bidirectional types, for modeling these situations, and we solve the corresponding control problems.\r\nIn a system with a dependent type, the dependencies between inputs and outputs are determined gradually through a game of the system against the controller. In a system with a bidirectional type, also the distinction between inputs and outputs is resolved dynamically by such a game. The game proceeds in several rounds. In each round the system and the controller choose to update some variables dependent on variables that have already been updated. The solution of the control problem for dependent and bidirectional types is based on algorithms for solving these games."}],"article_processing_charge":"No","scopus_import":"1","date_updated":"2023-05-08T10:20:19Z","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publication_identifier":{"isbn":["9783540424970"]},"publist_id":"74","oa_version":"None","year":"2001","publication":"Proceedings of the 12th International Conference on on Concurrency Theory","quality_controlled":"1","status":"public","intvolume":"      2154","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","month":"08","extern":"1","date_created":"2018-12-11T12:09:52Z","page":"566 - 581","language":[{"iso":"eng"}],"doi":"10.1007/3-540-44685-0_38","acknowledgement":"This research was supported in part by the SRC contract 99-TJ-683.003, the DARPA SEC grant F33615-C-98-3614, the MARCO GSRC grant 98-DT-660, the AFOSR MURI grant F49620-00-1-0327, and the NSF Theory grant CCR-9988172.","day":"13","type":"conference","author":[{"last_name":"De Alfaro","first_name":"Luca","full_name":"De Alfaro, Luca"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"first_name":"Freddy","full_name":"Mang, Freddy","last_name":"Mang"}],"alternative_title":["LNCS"],"citation":{"chicago":"De Alfaro, Luca, Thomas A Henzinger, and Freddy Mang. “The Control of Synchronous Systems, Part II.” In <i>Proceedings of the 12th International Conference on on Concurrency Theory</i>, 2154:566–81. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2001. <a href=\"https://doi.org/10.1007/3-540-44685-0_38\">https://doi.org/10.1007/3-540-44685-0_38</a>.","ista":"De Alfaro L, Henzinger TA, Mang F. 2001. The control of synchronous systems, Part II. Proceedings of the 12th International Conference on on Concurrency Theory. CONCUR: Concurrency Theory, LNCS, vol. 2154, 566–581.","ieee":"L. De Alfaro, T. A. Henzinger, and F. Mang, “The control of synchronous systems, Part II,” in <i>Proceedings of the 12th International Conference on on Concurrency Theory</i>, Aalborg, Denmark, 2001, vol. 2154, pp. 566–581.","mla":"De Alfaro, Luca, et al. “The Control of Synchronous Systems, Part II.” <i>Proceedings of the 12th International Conference on on Concurrency Theory</i>, vol. 2154, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2001, pp. 566–81, doi:<a href=\"https://doi.org/10.1007/3-540-44685-0_38\">10.1007/3-540-44685-0_38</a>.","short":"L. De Alfaro, T.A. Henzinger, F. Mang, in:, Proceedings of the 12th International Conference on on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2001, pp. 566–581.","ama":"De Alfaro L, Henzinger TA, Mang F. The control of synchronous systems, Part II. In: <i>Proceedings of the 12th International Conference on on Concurrency Theory</i>. Vol 2154. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2001:566-581. doi:<a href=\"https://doi.org/10.1007/3-540-44685-0_38\">10.1007/3-540-44685-0_38</a>","apa":"De Alfaro, L., Henzinger, T. A., &#38; Mang, F. (2001). The control of synchronous systems, Part II. In <i>Proceedings of the 12th International Conference on on Concurrency Theory</i> (Vol. 2154, pp. 566–581). Aalborg, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.1007/3-540-44685-0_38\">https://doi.org/10.1007/3-540-44685-0_38</a>"},"title":"The control of synchronous systems, Part II","conference":{"name":"CONCUR: Concurrency Theory","end_date":"2001-08-25","start_date":"2001-08-20","location":"Aalborg, Denmark"}}]