[{"main_file_link":[{"open_access":"1","url":"https://www.sciencedirect.com/science/article/pii/S0890540183710254?via%3Dihub"}],"oa":1,"publication_status":"published","volume":104,"issue":"1","article_processing_charge":"No","abstract":[{"lang":"eng","text":"The theory of the natural numbers with linear order and monadic predicates underlies propositional linear temporal logic. To study temporal logics that are suitable for reasoning about real-time systems, we combine this classical theory of infinite state sequences with a theory of discrete time, via a monotonic function that maps every state to its time. The resulting theory of timed state sequences is shown to be decidable, albeit nonelementary, and its expressive power is characterized by ω-regular sets. Several more expressive variants are proved to be highly undecidable. This framework allows us to classify a wide variety of real-time logics according to their complexity and expressiveness. Indeed, it follows that most formalisms proposed in the literature cannot be decided. We are, however, able to identify two elementary real-time temporal logics as expressively complete fragments of the theory of timed state sequences, and we present tableau-based decision procedures for checking validity. Consequently, these two formalisms are well-suited for the specification and verification of real-time systems.\r\n\r\nCopyright © 1993 Academic Press. All rights reserved."}],"_id":"4589","date_published":"1993-05-01T00:00:00Z","publication_identifier":{"eissn":["0890-5401"]},"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","date_updated":"2022-03-23T13:08:27Z","scopus_import":"1","oa_version":"Published Version","year":"1993","publist_id":"116","article_type":"original","publisher":"Elsevier","intvolume":"       104","status":"public","quality_controlled":"1","publication":"Information and Computation","page":"35 - 77","date_created":"2018-12-11T12:09:38Z","extern":"1","month":"05","acknowledgement":"We thank David Dill, Zohar Manna, and Amir Pnueli for helpful discussion.","doi":"10.1006/inco.1993.1025","language":[{"iso":"eng"}],"title":"Real-time logics: Complexity and expressiveness","citation":{"ieee":"R. Alur and T. A. Henzinger, “Real-time logics: Complexity and expressiveness,” <i>Information and Computation</i>, vol. 104, no. 1. Elsevier, pp. 35–77, 1993.","ista":"Alur R, Henzinger TA. 1993. Real-time logics: Complexity and expressiveness. Information and Computation. 104(1), 35–77.","chicago":"Alur, Rajeev, and Thomas A Henzinger. “Real-Time Logics: Complexity and Expressiveness.” <i>Information and Computation</i>. Elsevier, 1993. <a href=\"https://doi.org/10.1006/inco.1993.1025\">https://doi.org/10.1006/inco.1993.1025</a>.","mla":"Alur, Rajeev, and Thomas A. Henzinger. “Real-Time Logics: Complexity and Expressiveness.” <i>Information and Computation</i>, vol. 104, no. 1, Elsevier, 1993, pp. 35–77, doi:<a href=\"https://doi.org/10.1006/inco.1993.1025\">10.1006/inco.1993.1025</a>.","short":"R. Alur, T.A. Henzinger, Information and Computation 104 (1993) 35–77.","apa":"Alur, R., &#38; Henzinger, T. A. (1993). Real-time logics: Complexity and expressiveness. <i>Information and Computation</i>. Elsevier. <a href=\"https://doi.org/10.1006/inco.1993.1025\">https://doi.org/10.1006/inco.1993.1025</a>","ama":"Alur R, Henzinger TA. Real-time logics: Complexity and expressiveness. <i>Information and Computation</i>. 1993;104(1):35-77. doi:<a href=\"https://doi.org/10.1006/inco.1993.1025\">10.1006/inco.1993.1025</a>"},"author":[{"last_name":"Alur","full_name":"Alur, Rajeev","first_name":"Rajeev"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"}],"type":"journal_article","day":"01"},{"type":"journal_article","author":[{"full_name":"Edelsbrunner, Herbert","first_name":"Herbert","last_name":"Edelsbrunner","id":"3FB178DA-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-9823-6833"},{"last_name":"Preparata","first_name":"Franco","full_name":"Preparata, Franco"}],"day":"01","title":"Minimum polygonal separation","citation":{"ama":"Edelsbrunner H, Preparata F. Minimum polygonal separation. <i>Information and Computation</i>. 1988;77(3):218-232. doi:<a href=\"https://doi.org/10.1016/0890-5401(88)90049-1\">10.1016/0890-5401(88)90049-1</a>","apa":"Edelsbrunner, H., &#38; Preparata, F. (1988). Minimum polygonal separation. <i>Information and Computation</i>. Elsevier. <a href=\"https://doi.org/10.1016/0890-5401(88)90049-1\">https://doi.org/10.1016/0890-5401(88)90049-1</a>","short":"H. Edelsbrunner, F. Preparata, Information and Computation 77 (1988) 218–232.","mla":"Edelsbrunner, Herbert, and Franco Preparata. “Minimum Polygonal Separation.” <i>Information and Computation</i>, vol. 77, no. 3, Elsevier, 1988, pp. 218–32, doi:<a href=\"https://doi.org/10.1016/0890-5401(88)90049-1\">10.1016/0890-5401(88)90049-1</a>.","chicago":"Edelsbrunner, Herbert, and Franco Preparata. “Minimum Polygonal Separation.” <i>Information and Computation</i>. Elsevier, 1988. <a href=\"https://doi.org/10.1016/0890-5401(88)90049-1\">https://doi.org/10.1016/0890-5401(88)90049-1</a>.","ista":"Edelsbrunner H, Preparata F. 1988. Minimum polygonal separation. Information and Computation. 77(3), 218–232.","ieee":"H. Edelsbrunner and F. Preparata, “Minimum polygonal separation,” <i>Information and Computation</i>, vol. 77, no. 3. Elsevier, pp. 218–232, 1988."},"doi":"10.1016/0890-5401(88)90049-1","language":[{"iso":"eng"}],"acknowledgement":"Research of the first author is supported by Amoco Fnd. Fat. Dev. Comput. Sci. l-6-44862; research of the second author is supported by NSF Grant ECS 84-10902.","date_created":"2018-12-11T12:06:53Z","month":"06","extern":"1","page":"218 - 232","intvolume":"        77","status":"public","publication":"Information and Computation","quality_controlled":"1","publisher":"Elsevier","oa_version":"None","year":"1988","article_type":"original","publist_id":"2029","publication_identifier":{"eissn":["0890-5401"]},"scopus_import":"1","date_updated":"2022-02-08T10:36:30Z","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","date_published":"1988-06-01T00:00:00Z","_id":"4090","abstract":[{"lang":"eng","text":"In this paper we study the problem of polygonal separation in the plane, i.e., finding a convex polygon with minimum number k of sides separating two given finite point sets (k-separator), if it exists. We show that for k = Θ(n),  is a lower bound to the running time of any algorithm for this problem, and exhibit two algorithms of distinctly different flavors. The first relies on an O(n log n)-time preprocessing task, which constructs the convex hull of the internal set and a nested star-shaped polygon determined by the external set; the k-separator is contained in the annulus between the boundaries of these two polygons and is constructed in additional linear time. The second algorithm adapts the prune-and-search approach, and constructs, in each iteration, one side of the separator; its running time is O(kn), but the separator may have one more side than the minimum."}],"article_processing_charge":"No","issue":"3","volume":77,"main_file_link":[{"open_access":"1","url":"https://www.sciencedirect.com/science/article/pii/0890540188900491?via%3Dihub"}],"oa":1,"publication_status":"published"}]