{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:08:22Z","timestamp":1750219702321,"version":"3.41.0"},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2024,6,18]],"date-time":"2024-06-18T00:00:00Z","timestamp":1718668800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2024,6,30]]},"abstract":"<jats:p>The behavior and architecture of large scale discrete state systems found in computer software and hardware can be specified and analyzed using a particular class of primitive recursive functions. This article begins with an illustration of the utility of the method via a number of small examples and then via longer specification and verification of the \u201cPaxos\u201d distributed consensus algorithm [<jats:xref ref-type=\"bibr\">26<\/jats:xref>]. The \u201csequence maps\u201d are then shown to provide an alternative representation of deterministic state machines and products of state machines.<\/jats:p><jats:p>Distributed and composite systems, parallel and concurrent computation, and real-time behavior can all be specified naturally with these methods\u2014which require neither extensions to the classical state machine model nor any axiomatic methods or other techniques from formal logic or other foundational methods. Compared to state diagrams or tables or the standard set-tuple-transition-maps, sequence maps are more concise and better suited to describing the behavior and compositional architecture of computer systems. Staying strictly within the boundaries of classical deterministic state machines anchors the methods to the algebraic structures of automata and makes the specifications faithful to engineering practice.<\/jats:p>","DOI":"10.1145\/3633786","type":"journal-article","created":{"date-parts":[[2023,11,22]],"date-time":"2023-11-22T12:32:27Z","timestamp":1700656347000},"page":"1-23","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["State Machines for Large Scale Computer Software and Systems"],"prefix":"10.1145","volume":"36","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5085-9794","authenticated-orcid":false,"given":"Victor","family":"Yodaiken","sequence":"first","affiliation":[{"name":"Independent Researcher, Austin, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,6,18]]},"reference":[{"issue":"1","key":"e_1_3_4_2_2","article-title":"Composing specifications","volume":"15","author":"Abadi Martin","year":"1993","unstructured":"Martin Abadi and Leslie Lamport. 1993. Composing specifications. Transactions on Programming Languages and Systems 15, 1(1993), 73\u2013132.","journal-title":"Transactions on Programming Languages and Systems"},{"key":"e_1_3_4_3_2","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2013.418"},{"key":"e_1_3_4_4_2","doi-asserted-by":"publisher","DOI":"10.5555\/1098643"},{"key":"e_1_3_4_5_2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(91)90139-S"},{"key":"e_1_3_4_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/800217.806617"},{"key":"e_1_3_4_7_2","unstructured":"Manfred Broy. 1997. The Specification of System Components by State Transition Diagrams. TUM-I9729 Institut f\u00fcr Informatik Technische Universit\u00e4t M\u00fcnchen."},{"key":"e_1_3_4_8_2","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/bxq005"},{"key":"e_1_3_4_9_2","doi-asserted-by":"crossref","unstructured":"Saksham Chand Yanhong A. Liu and Scott D. Stoller. 2016. Formal verification of multi-paxos for distributed consensus. In Proceedings of the 21st International Symposium on Formal Methods (FM\u201916) (Lecture Notes in Computer Science) Springer-Verlag 119\u2013136.","DOI":"10.1007\/978-3-319-48989-6_8"},{"key":"e_1_3_4_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/1281100.1281103"},{"key":"e_1_3_4_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/173668.168629"},{"key":"e_1_3_4_12_2","first-page":"117","volume-title":"Proceedings of the 10th Annual Symposium on Principles of Programming Languages","author":"Clarke E. M.","year":"1983","unstructured":"E. M. Clarke, Emerson A., and A. P. Sistla. 1983. Automatic verification of finite-state concurrent systems using temporal logic specifications: A practical approach. In Proceedings of the 10th Annual Symposium on Principles of Programming Languages. 117\u2013119."},{"key":"e_1_3_4_13_2","first-page":"229","volume-title":"Proceedings of the 3rd Symposium on Operating Systems Design and Implementation (OSDI\u201999)","author":"Dougan Cort","year":"1999","unstructured":"Cort Dougan, Paul Mackerras, and Victor Yodaiken. 1999. Optimizing the idle task and other MMU tricks. In Proceedings of the 3rd Symposium on Operating Systems Design and Implementation (OSDI\u201999). USENIX Association, 229\u2013237."},{"key":"e_1_3_4_14_2","unstructured":"Cort Dougan and Victor Yodaiken. 2016. METHOD TIME CONSUMER SYSTEM AND COMPUTER PROGRAM PRODUCT FOR MAINTAINING ACCURATE TIME ON AN IDEAL CLOCK. US Patents and Trademarks Office Patent number 20160238999."},{"key":"e_1_3_4_15_2","volume-title":"Recursiveness","author":"Eilenberg S.","year":"1970","unstructured":"S. Eilenberg and Calvin Elgot. 1970. Recursiveness. Academic Press, New York."},{"key":"e_1_3_4_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-61611-2"},{"key":"e_1_3_4_17_2","volume-title":"Algebraic Theory of Automata","author":"Ginzburg A.","year":"1968","unstructured":"A. Ginzburg. 1968. Algebraic Theory of Automata. Academic Press, New York."},{"key":"e_1_3_4_18_2","doi-asserted-by":"publisher","unstructured":"Aman Goel and Karem A. Sakallah. 2021. Towards an automatic proof of lamport\u2019s paxos. In Formal Methods in Computer-Aided Design (FMCAD) New Haven CT 112\u2013122. DOI:10.34727\/2021\/isbn.978-3-85448-046-4_20","DOI":"10.34727\/2021\/isbn.978-3-85448-046-4_20"},{"key":"e_1_3_4_19_2","doi-asserted-by":"publisher","unstructured":"Jim Gray and Leslie Lamport. 2006. Consensus on transaction commit. ACM Trans. Database Syst. 31 1 (March 2006) 133\u2013160. DOI:10.1145\/1132863.1132867","DOI":"10.1145\/1132863.1132867"},{"key":"e_1_3_4_20_2","volume-title":"Statecharts: A Visual Formalism for Complex Systems","author":"Harel D.","year":"1984","unstructured":"D. Harel. 1984. Statecharts: A Visual Formalism for Complex Systems. Technical Report. Weizmann Institute."},{"key":"e_1_3_4_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/235321.235322"},{"key":"e_1_3_4_22_2","first-page":"115","volume-title":"Proceedings of the Sequential Machines: Selected Papers","author":"Hartmanis J.","year":"1964","unstructured":"J. Hartmanis. 1964. Loop-free structure of sequential machines. In Proceedings of the Sequential Machines: Selected Papers. E.F. Moore (Ed.), Addison-Welsey, Reading MA, 115\u2013156."},{"key":"e_1_3_4_23_2","volume-title":"Algebraic Structure Theory of Sequential Machines","author":"Hartmanis J.","year":"1966","unstructured":"J. Hartmanis and R. E. Stearns. 1966. Algebraic Structure Theory of Sequential Machines. Prentice-Hall, Englewood Cliffs, N.J."},{"key":"e_1_3_4_24_2","volume-title":"Algebraic Automata Theory","author":"Holcombe W. M. L.","year":"1983","unstructured":"W. M. L. Holcombe. 1983. Algebraic Automata Theory. Cambridge University Press."},{"key":"e_1_3_4_25_2","volume-title":"Introduction to Automata Theory, Languages, and Computation","author":"Hopcroft John E.","year":"1979","unstructured":"John E. Hopcroft and Jeffrey D. Ullman. 1979. Introduction to Automata Theory, Languages, and Computation. Addison-Welsey, Reading MA."},{"key":"e_1_3_4_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"e_1_3_4_27_2","first-page":"51","article-title":"Paxos made simple","author":"Lamport Leslie","year":"2001","unstructured":"Leslie Lamport. 2001. Paxos made simple. ACM SIGACT News (Distributed Computing Column) 32, 4 (Whole Number 121, December 2001)(2001), 51\u201358. Retrieved from https:\/\/www.microsoft.com\/en-us\/research\/publication\/paxos-made-simple\/","journal-title":"ACM SIGACT News (Distributed Computing Column) 32, 4 (Whole Number 121, December 2001)"},{"key":"e_1_3_4_28_2","volume-title":"Introduction to the Theory of Nested Transactions","author":"N. A. Lynch,","year":"1986","unstructured":"A. Lynch, N. and M. Merrrit. 1986. Introduction to the Theory of Nested Transactions. Technical Report TR-367. Laboratory for Computer Science, MIT."},{"key":"e_1_3_4_29_2","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/7728.001.0001"},{"key":"e_1_3_4_30_2","volume-title":"On the Krohn-Rhodes Cascaded Decomposition Theorem","author":"Maler Oded","year":"2010","unstructured":"Oded Maler. 2010. On the Krohn-Rhodes Cascaded Decomposition Theorem. Springer-Verlag, Berlin."},{"key":"e_1_3_4_31_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1007\/3-540-09510-1_31","volume-title":"Proceedings of the 6th International Colloquium on Automata, Languages, and Programming","volume":"71","author":"Manna Z.","year":"1979","unstructured":"Z. Manna and A. Pnueli. 1979. The modal logic of programs. In Proceedings of the 6th International Colloquium on Automata, Languages, and Programming(Lecture Notes in Computer Science, Vol. 71). Springer-Verlag, New York, 385\u2013408."},{"issue":"2","key":"e_1_3_4_32_2","article-title":"Finite automata and their decision problems","volume":"3","author":"O. Rabin M.","year":"1959","unstructured":"Rabin M. O. and Dana Scott. 1959. Finite automata and their decision problems. IBM Journal of Research and Development 3, 2(1959), 114\u2013125.","journal-title":"IBM Journal of Research and Development"},{"key":"e_1_3_4_33_2","doi-asserted-by":"publisher","DOI":"10.5555\/1102050"},{"key":"e_1_3_4_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/361598.361623"},{"key":"e_1_3_4_35_2","volume-title":"Recursive Functions","author":"Peter Rozsa","year":"1967","unstructured":"Rozsa Peter. 1967. Recursive Functions. Academic Press, New York."},{"key":"e_1_3_4_36_2","doi-asserted-by":"publisher","DOI":"10.5555\/539249"},{"key":"e_1_3_4_37_2","doi-asserted-by":"publisher","DOI":"10.5555\/576708"},{"key":"e_1_3_4_38_2","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the Current Trends in Concurrency","volume":"224","author":"Pnueli A.","year":"1985","unstructured":"A. Pnueli. 1985. Applications of temporal logic to the specification and verification of reactive systems: A survey of curent trends. In Proceedings of the Current Trends in Concurrency. J. W. de Bakker (Ed.), Lecture Notes in Computer Science, Vol. 224. Springer-Verlag."},{"key":"e_1_3_4_39_2","doi-asserted-by":"publisher","DOI":"10.1016\/0306-4379(83)90017-0"},{"key":"e_1_3_4_40_2","volume-title":"Mathematical Logic","author":"Shoenfield Joseph R.","year":"1967","unstructured":"Joseph R. Shoenfield. 1967. Mathematical Logic. Addison-Wesley."},{"key":"e_1_3_4_41_2","first-page":"1","volume-title":"Proceedings of the Cerebral Mechanisms in Behavior","author":"Neumann John von","year":"1941","unstructured":"John von Neumann. 1941. The general and logical theory of automata. In Proceedings of the Cerebral Mechanisms in Behavior. Wiley, 1\u201341."},{"key":"e_1_3_4_42_2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139856065","volume-title":"Modern Computer Algebra:","author":"Gathen J. von zur","year":"2013","unstructured":"J. von zur Gathen and J. Gerhard. 2013. Modern Computer Algebra:. Cambridge University Press. 2013431595 Retrieved from https:\/\/books.google.com\/books?id=7fE9baKyqSEC"},{"key":"e_1_3_4_43_2","first-page":"591","volume-title":"Proceedings of the CAV (DIMACS\/AMS Volume)","author":"Yodaiken Victor","year":"1990","unstructured":"Victor Yodaiken. 1990. The algebraic feedback product of automata. a state machine based model of concurrent systems. In Proceedings of the CAV (DIMACS\/AMS Volume). Springer Science and Business Media, New Brunswick, NJ, 591\u2013614."},{"key":"e_1_3_4_44_2","volume-title":"Proceedings of the Papers from the DIMACS Workshop on Computer Aided Verification","author":"Yodaiken Victor","year":"1991","unstructured":"Victor Yodaiken. 1991. The algebraic feedback product of automata. In Proceedings of the Papers from the DIMACS Workshop on Computer Aided Verification. American Mathematical Society."},{"issue":"2","key":"e_1_3_4_45_2","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1016\/0020-0190(91)90011-6","article-title":"Modal functions for concise definition of state machines and products","volume":"40","author":"Yodaiken Victor","year":"1991","unstructured":"Victor Yodaiken. 1991. Modal functions for concise definition of state machines and products. Information Processing Letters 40, 2(1991), 65\u201372. IFPLAT","journal-title":"Information Processing Letters"},{"key":"e_1_3_4_46_2","volume-title":"Proceedings of the USENIX 1997 Annual Technical Conference (USENIX ATC 97)","author":"Yodaiken Victor","year":"1997","unstructured":"Victor Yodaiken and Michael Barabanov. 1997. Real-time. In Proceedings of the USENIX 1997 Annual Technical Conference (USENIX ATC 97). USENIX Association, Anaheim, CA. Retrieved from https:\/\/www.usenix.org\/conference\/usenix-1997-annual-technical-conference\/real-time"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3633786","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3633786","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:35:48Z","timestamp":1750178148000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3633786"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,18]]},"references-count":45,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2024,6,30]]}},"alternative-id":["10.1145\/3633786"],"URL":"https:\/\/doi.org\/10.1145\/3633786","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2024,6,18]]},"assertion":[{"value":"2022-06-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-11-16","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-06-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}