{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T16:51:24Z","timestamp":1694623884431},"reference-count":15,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[1995,11,1]],"date-time":"1995-11-01T00:00:00Z","timestamp":815184000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[1995,11]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>This paper is concerned with specifications expressed in propositional temporal logic with finite past extension. The variables of the specifications are partitioned into input variables, the value of which is determined by the environment, output variables, the value of which may be required by the environment, and internal variables. We present a method to synthesise temporal specifications, i.e. to rewrite them into a form from which a valuation for the output variables may be generated from the input values without backtracking. The transformed specification characterises the same set of input\/output functions as the original specification, but in a more explicit way. A simple interpreter chooses the actual function to be used.<\/jats:p>","DOI":"10.1007\/bf01210997","type":"journal-article","created":{"date-parts":[[2005,2,25]],"date-time":"2005-02-25T12:43:49Z","timestamp":1109335429000},"page":"587-619","source":"Crossref","is-referenced-by-count":1,"title":["A transformation-based synthesis of temporal specifications"],"prefix":"10.1145","volume":"7","author":[{"given":"Philippe","family":"No\u00ebl","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Manchester, Manchester, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","first-page":"94","volume-title":"REX Workshop on Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness (LNCS Volume 430)","author":"Barringer H.","year":"1989"},{"key":"e_1_2_1_2_2_2","volume-title":"Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning","author":"Barringer H.","year":"1991"},{"key":"e_1_2_1_2_3_2","unstructured":"Chang C.-L. and Lee R. C.-T.: Symbolic Logic and Mechanical Theorem Proving . Academic Press 1973."},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(84)80047-9"},{"key":"e_1_2_1_2_5_2","volume-title":"Proceedings of the International Joint Conference on Artificial Intelligence","author":"Fisher M.","year":"1991"},{"key":"e_1_2_1_2_6_2","unstructured":"Fisher M. and No\u00ebl P.: Transformation and Synthesis in MetateM . MetateM project report Department of Computer Science University of Manchester February 1992."},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Hossley A. and Rackoff C.: The Emptiness Problem for Automata on Infinite Trees. In 13th IEEE Symposium on Switching aARD EDITnd Automata Theory pages 121\u2013124 1972.","DOI":"10.1109\/SWAT.1972.28"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Lichtendtein O. Pnueli A. and Zuck L.: The Glory of the Past. In Proc. Workshop on Logic of Programs pages 196\u2013218. Springer-Verlag 1985. LNCS 193.","DOI":"10.1007\/3-540-15648-8_16"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Noel P.: A Method for the Determinisation of Propositional Temporal Formulae. In T.P. Clement and P.-K. Lau editors Logic Program Synthesis and Transformation . Springer-Verlag 1992. LOPSTR 91.","DOI":"10.1007\/978-1-4471-3494-7_20"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Pnueli A.: The Temporal Logic of Programs. In Proceedings of the Eighteenth Symposium on the Foundations of Computer Science Providence November 1977.","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Pnueli A. and Rosner R.: On the Synthesis of a Reactive Module. In 16th ACM POPL pages 179\u2013190 January 1989.","DOI":"10.1145\/75277.75293"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Safra S.: On the Complexity of \u03c9 -automata. In 29th IEEE Symposium on Foundation of Computer Science 1988.","DOI":"10.1109\/SFCS.1988.21948"},{"key":"e_1_2_1_2_13_2","unstructured":"Wikstr\u00f6m \u00c5.: Functional Programming using ML . Prentice-Hall International 1987."},{"key":"e_1_2_1_2_14_2","first-page":"119","article-title":"The Tableau Method for Temporal Logic: an Overview","volume":"110","author":"Wolper P.","year":"1985","journal-title":"Logique et Analyse"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Wolper P.: On the Relation of Programs and Computations to Models of Temporal Logic. In Temporal Logic in Specification pages 75\u2013123. Springer-Verlag 1987. LNCS 398.","DOI":"10.1007\/3-540-51803-7_23"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01210997.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01210997\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/BF01210997","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:24:29Z","timestamp":1641482669000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/BF01210997"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,11]]},"references-count":15,"journal-issue":{"issue":"6","published-print":{"date-parts":[[1995,11]]}},"alternative-id":["10.1007\/BF01210997"],"URL":"https:\/\/doi.org\/10.1007\/bf01210997","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995,11]]}}}