{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,6]],"date-time":"2026-04-06T11:06:36Z","timestamp":1775473596057,"version":"3.50.1"},"reference-count":93,"publisher":"Emerald","issue":"2","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022,12,1]]},"abstract":"<jats:p>Traditional computer science is Boolean: a Turing machine accepts or rejects its input, and logic assertions are true or false. A primary use of logic in computer science has been the specification and verification of reactive systems. There, desired behaviors of systems are formally specified by temporal-logic formulas, and questions about systems and their behaviors are reduced to questions like satisfiability and model checking. While correctness is binary, many questions we want to ask about systems are multi-valued. The multi-valued setting arises directly in systems with quantitative aspects, for example systems with fuzzy assignments or stochastic dynamics, and arises also in Boolean systems, where it origins from the semantics of the specification formalism. In particular, beyond checking whether a system satisfies its specification, we may want to evaluate the quality in which the specification is satisfied. The term \u201cquality\u201d may refer to many aspects of the behavior: we may want to prioritize different satisfaction alternatives, refer to delays, costs, and many more. In recent years, we have seen a growing effort in the formal-method community to shift from Boolean specification formalisms to multi-valued ones.<\/jats:p>\n                  <jats:p>The shift involves a development of multi-valued temporal logics as well as algorithms and tools for reasoning about such logics.<\/jats:p>\n                  <jats:p>This survey describes the basics of specification and verification of reactive systems, and the automata-theoretic approach for them: by translating temporal-logic formulas to automata, one reduces questions like satisfiability and model checking to decision problems on automata, like non-emptiness and language containment.<\/jats:p>\n                  <jats:p>We first describe the Boolean setting: temporal logics, and their applications in specification and verification. Since we care about on-going behaviors of non-terminating systems, the formalisms we study specify infinite computations, and we focus on the theoretical properties of automata on infinite words. The transition from finite to infinite words results in a beautiful mathematical model with much richer combinatorial properties. We then describe two multi-valued settings. The first is based on finite lattices and the second on arbitrary functions over [0, 1]. In both settings, the goal is to refine the Boolean correctness query to a quantitative-evaluation query. Accordingly, the formalisms we introduce are such that the satisfaction value of a temporal-logic formula in a model, or the membership value of a word in the language of an automaton, are multi valued, and classical decision problems become search problems.<\/jats:p>","DOI":"10.1561\/0400000083","type":"journal-article","created":{"date-parts":[[2022,12,1]],"date-time":"2022-12-01T03:49:16Z","timestamp":1669866556000},"page":"126-228","source":"Crossref","is-referenced-by-count":1,"title":["Multi-Valued Reasoning about Reactive Systems"],"prefix":"10.1561","volume":"15","author":[{"given":"Orna","family":"Kupferman","sequence":"first","affiliation":[{"name":"The Hebrew University ,","place":["Israel"]}]}],"member":"140","published-online":{"date-parts":[[2022,12,1]]},"reference":[{"key":"2026040605562786100_ref001","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/978-3-540-27836-8_11","article-title":"Linear and branching metrics for quantitative transition systems","author":"de Alfaro","year":"2004","journal-title":"Proc. 31st Int. Colloq. on Automata, Languages, and Programming"},{"key":"2026040605562786100_ref002","doi-asserted-by":"crossref","first-page":"482","DOI":"10.1007\/978-3-642-24372-1_37","article-title":"What\u2019s decidable about weighted automata?","volume":"6996","author":"Almagor","year":"2011","journal-title":"9th Int. Symp. on Automated Technology for Verification and Analysis"},{"key":"2026040605562786100_ref003","first-page":"15","article-title":"Formalizing and reasoning about quality","volume":"7966","author":"Almagor","year":"2013","journal-title":"Proc. 40th Int. Colloq. on Automata, Languages, and Programming"},{"issue":"3","key":"2026040605562786100_ref004","first-page":"56","article-title":"Formalizing and reasoning about quality","volume":"63","author":"Almagor","journal-title":"Journal of the ACM"},{"issue":"3","key":"2026040605562786100_ref005","doi-asserted-by":"crossref","first-page":"547","DOI":"10.1007\/s10626-017-0242-0","article-title":"Latticed-LTL synthesis in the presence of noisy inputs","volume":"27","author":"Almagor","journal-title":"Discrete Event Dynamic Systems"},{"key":"2026040605562786100_ref006","doi-asserted-by":"crossref","first-page":"240","DOI":"10.1007\/978-3-540-70545-1_23","article-title":"Ranking automata and games for prioritized requirements","volume":"5123","author":"Alur","year":"2008","journal-title":"Proc. 20th Int. Conf. on Computer Aided Verification"},{"key":"2026040605562786100_ref007","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511804090","author":"Arora","year":"2009","journal-title":"Computational Complexity - A Modern Approach"},{"key":"2026040605562786100_ref008","first-page":"140","article-title":"Better quality in synthesis through quantitative objectives","volume":"5643","author":"Bloem","year":"2009","journal-title":"Proc. 21st Int. Conf. on Computer Aided Verification"},{"key":"2026040605562786100_ref009","first-page":"150","article-title":"Improved Ramsey-based B\u00fcchi complementation","volume":"7213","author":"Breuers","year":"2012","journal-title":"Proc. 15th Int. Conf. on Foun-dations of Software Science and Computation Structures"},{"key":"2026040605562786100_ref010","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1007\/978-3-540-27836-8_26","article-title":"Model checking with multi-valued logics","volume":"3142","author":"Bruns","year":"2004","journal-title":"Proc. 31st Int. Colloq. on Automata, Languages, and Programming"},{"key":"2026040605562786100_ref011","first-page":"1","article-title":"On a decision method in restricted second order arith-metic","author":"B\u00fcchi","year":"1962","journal-title":"Proc. Int. Congress on Logic, Method, and Philosophy of Science. 1960"},{"key":"2026040605562786100_ref012","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1007\/978-3-642-22110-1_20","article-title":"Quantitative synthesis for concurrent programs","author":"Cern\u00fd","year":"2011","journal-title":"Proc. 23rd Int. Conf. on Computer Aided Verification"},{"issue":"1","key":"2026040605562786100_ref013","doi-asserted-by":"crossref","first-page":"114","DOI":"10.1145\/322234.322243","article-title":"Alternation","volume":"28","author":"Chandra","journal-title":"Journal of the Association for Computing Machinery"},{"key":"2026040605562786100_ref014","first-page":"385","article-title":"Quantative lan-guages","author":"Chatterjee","year":"2008","journal-title":"Proc. 17th Annual Conf. of the European Association for Computer Science Logic"},{"key":"2026040605562786100_ref015","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/S0022-0000(74)80051-6","article-title":"Theories of automata on \u03c9-tapes: A simplified approach","volume":"8","author":"Choueka","journal-title":"Journal of Computer and Systems Science"},{"issue":"4","key":"2026040605562786100_ref016","doi-asserted-by":"crossref","first-page":"410","DOI":"10.1007\/s100090050046","article-title":"NuSMV: A new symbolic model checker","volume":"2","author":"Cimatti","journal-title":"Software Tools for Technology Transfer"},{"issue":"2","key":"2026040605562786100_ref017","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","article-title":"Automatic verification of finite-state concurrent systems using temporal logic specifi-cations","volume":"8","author":"Clarke","journal-title":"ACM Transactions on Programming Languagues and Systems"},{"key":"2026040605562786100_ref018","author":"Clarke","year":"2018","journal-title":"Model Checking, Second Edition"},{"key":"2026040605562786100_ref019","author":"Cormen","year":"1990","journal-title":"Introduction to Algo-rithms"},{"key":"2026040605562786100_ref020","author":"Spinellis","year":"2006","journal-title":"Code Quality: The Open Source Perspective"},{"key":"2026040605562786100_ref021","doi-asserted-by":"crossref","first-page":"92","DOI":"10.1007\/978-3-642-33386-6_9","article-title":"On temporal logic and signal processing","author":"Donz\u00e9","year":"2012","journal-title":"10th Int. Symp. on Automated Technology for Verification and Analysis"},{"key":"2026040605562786100_ref022","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-01492-5","author":"Droste","year":"2009","journal-title":"Handbook of Weighted Automata"},{"key":"2026040605562786100_ref023","first-page":"411","article-title":"A framework for multi-valued reasoning over inconsistent viewpoints","author":"Easterbrook","year":"2001","journal-title":"Proc. 23rd Int. Conf. on Software Engineering"},{"key":"2026040605562786100_ref024","doi-asserted-by":"crossref","first-page":"328","DOI":"10.1109\/SFCS.1988.21949","article-title":"The complexity of tree automata and logics of programs","author":"Emerson","year":"1988","journal-title":"Proc. 29th IEEE Symp. on Foundations of Computer Science"},{"key":"2026040605562786100_ref025","doi-asserted-by":"crossref","first-page":"368","DOI":"10.1109\/SFCS.1991.185392","article-title":"Tree automata, \u00b5-calculus and deter-minacy","author":"Emerson","year":"1991","journal-title":"Proc. 32nd IEEE Symp. on Foundations of Computer Science"},{"key":"2026040605562786100_ref026","first-page":"84","article-title":"Modalities for model checking: Branch-ing time logic strikes back","author":"Emerson","year":"1985","journal-title":"Proc. 12th ACM Symp. on Princi-ples of Programming Languages"},{"key":"2026040605562786100_ref027","article-title":"Temporal model checking under generalized fairness constraints","author":"Emerson","journal-title":"Proc. 18th Hawaii Int. Conf. on System Sciences"},{"issue":"3","key":"2026040605562786100_ref028","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1016\/j.entcs.2008.11.019","article-title":"Model checking quantita-tive linear time logic","volume":"220","author":"Faella","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"2026040605562786100_ref029","first-page":"133","article-title":"Finite-valued weighted automata","author":"Filiot","year":"2014","journal-title":"Proc. 34th Conf. on Foundations of Software Tech-nology and Theoretical Computer Science"},{"key":"2026040605562786100_ref030","first-page":"248","article-title":"Unifying B\u00fcchi complementation constructions","author":"Fogarty","year":"2011","journal-title":"Proc. 20th Annual Conf. of the European Association for Computer Science Logic"},{"issue":"4","key":"2026040605562786100_ref031","doi-asserted-by":"crossref","first-page":"851","DOI":"10.1142\/S0129054106004145","article-title":"B\u00fcchi complementa-tion made tighter","volume":"17","author":"Friedgut","journal-title":"Int. J. Found. Comput. Sci."},{"key":"2026040605562786100_ref032","first-page":"35","article-title":"Constructing B\u00fcchi automata from linear temporal logic using simulation relations for alternating B\u00fcchi automata","author":"Fritz","year":"2003","journal-title":"Proc. 8th Int. Conf. on Implementation and Application of Automata"},{"key":"2026040605562786100_ref033","first-page":"163","article-title":"On the temporal analysis of fairness","author":"Gabbay","year":"1980","journal-title":"Proc. 7th ACM Symp. on Principles of Programming Languages"},{"key":"2026040605562786100_ref034","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/3-540-44585-4_6","article-title":"Fast LTL to B\u00fcchi automata transla-tion","volume":"2102","author":"Gastin","year":"2001","journal-title":"Proc. 13th Int. Conf. on Computer Aided Verification"},{"key":"2026040605562786100_ref035","first-page":"3","article-title":"Simple on-the-fly automatic verification of linear temporal logic","author":"Gerth","year":"1995","journal-title":"Protocol Speci-fication, Testing, and Verification"},{"key":"2026040605562786100_ref036","first-page":"308","article-title":"From states to transitions: Im-proving translation of LTL formulae to B\u00fcchi automata","volume":"2529","author":"Giannakopoulou","year":"2002","journal-title":"Proc. 22nd International Conference on Formal Techniques for Net-worked and Distributed Systems"},{"key":"2026040605562786100_ref037","first-page":"423","article-title":"COSPAN","volume":"1102","author":"Hardin","year":"1996","journal-title":"Proc. 8th Int. Conf. on Computer Aided Verification"},{"key":"2026040605562786100_ref038","first-page":"477","article-title":"On the development of reactive systems","volume":"F-13","author":"Harel","journal-title":"Logics and Models of Concurrent Systems"},{"issue":"5","key":"2026040605562786100_ref039","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","article-title":"The model checker SPIN","volume":"23","author":"Holzmann","journal-title":"IEEE Transactions on Software Engineering"},{"key":"2026040605562786100_ref040","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1016\/j.entcs.2004.08.003","article-title":"Consistent partial model checking","volume":"73","author":"Huth","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"2026040605562786100_ref041","volume-title":"IEEE standard multivalue logic system for VHDL model interoperability (Std_logic_1164)","author":"IEEE","year":"1993"},{"key":"2026040605562786100_ref042","first-page":"935","article-title":"Nondeterministic space is closed under comple-ment","volume":"17","author":"Immerman","journal-title":"Information and Computation"},{"key":"2026040605562786100_ref043","doi-asserted-by":"crossref","first-page":"724","DOI":"10.1007\/978-3-540-70575-8_59","article-title":"Complementation, disambiguation, and determinization of B\u00fcchi automata unified","volume":"5126","author":"K\u00e4hler","year":"2008","journal-title":"Proc. 35th Int. Colloq. on Automata, Languages, and Programming"},{"key":"2026040605562786100_ref044","article-title":"Tense logic and the theory of order","author":"Kamp","year":"1968"},{"key":"2026040605562786100_ref045","author":"Kans","year":"2002","journal-title":"Metrics and Models in Software Quality Engineering"},{"key":"2026040605562786100_ref046","first-page":"589","article-title":"Deciding unambiguity and sequen-tiality of polynomially ambiguous min-plus automata","author":"Kirsten","year":"2009","journal-title":"26th International Symposium on Theoretical Aspects of Computer Sci-ence, STACS 2009, February 26-28, 2009, Freiburg, Germany, Proceedings"},{"key":"2026040605562786100_ref047","doi-asserted-by":"crossref","first-page":"358","DOI":"10.1109\/SFCS.1991.185391","article-title":"Progress measures for complementation of \u03c9-auto-mata with applications to temporal logic","author":"Klarlund","year":"1991","journal-title":"Proc. 32nd IEEE Symp. on Foundations of Computer Science"},{"key":"2026040605562786100_ref048","first-page":"7","article-title":"Deterministic automata for the (f, g)-fragment of LTL","volume":"7358","author":"Kret\u00ednsk\u00fd","year":"2012","journal-title":"Proc. 24th Int. Conf. on Computer Aided Verification"},{"key":"2026040605562786100_ref049","first-page":"378","volume":"834","author":"Krishnan","year":"1994","journal-title":"\u03c9"},{"issue":"3","key":"2026040605562786100_ref050","doi-asserted-by":"crossref","first-page":"405","DOI":"10.1142\/S0218196794000063","article-title":"The equality problem for rational series with multiplici-ties in the tropical semiring is undecidable","volume":"4","author":"Krob","journal-title":"International Journal of Algebra and Computation"},{"key":"2026040605562786100_ref051","first-page":"107","article-title":"Automata theory and model checking","volume":"2018","author":"Kupferman","journal-title":"Hand-book of Model Checking"},{"key":"2026040605562786100_ref052","first-page":"199","article-title":"Lattice automata","volume":"4349","author":"Kupferman","year":"2007","journal-title":"Proc. 8th Int. Conf. on Verification, Model Checking, and Abstract Interpretation"},{"issue":"2","key":"2026040605562786100_ref053","first-page":"408","article-title":"Weak alternating automata are not that weak","volume":"2","author":"Kupferman","journal-title":"ACM Transactions on Computational Logic"},{"key":"2026040605562786100_ref054","first-page":"206","article-title":"Complementation constructions for nondeterministic automata on infinite words","volume":"3440","author":"Kupferman","year":"2005","journal-title":"Proc. 11th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems"},{"issue":"2","key":"2026040605562786100_ref055","doi-asserted-by":"crossref","first-page":"312","DOI":"10.1145\/333979.333987","article-title":"An automata-theoretic approach to branching-time model checking","volume":"47","author":"Kupferman","journal-title":"Journal of the ACM"},{"key":"2026040605562786100_ref056","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1016\/0022-0000(87)90036-5","article-title":"Complementing deterministic B\u00fcchi automata in polynomial time","volume":"35","author":"Kurshan","journal-title":"Journal of Computer and Systems Science"},{"key":"2026040605562786100_ref057","author":"Kurshan","year":"1994","journal-title":"Computer Aided Verification of Coordinating Pro-cesses"},{"key":"2026040605562786100_ref058","doi-asserted-by":"crossref","first-page":"376","DOI":"10.1007\/BF01691063","article-title":"Decision problems for \u03c9\u2013automata","volume":"3","author":"Landweber","journal-title":"Mathematical Systems Theory"},{"issue":"2","key":"2026040605562786100_ref059","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1016\/0304-3975(95)00035-U","article-title":"A hierarchy of temporal logics with past","volume":"148","author":"Laroussinie","journal-title":"Theoretical Computer Science"},{"key":"2026040605562786100_ref060","first-page":"97","article-title":"Checking that finite state con-current programs satisfy their linear specification","author":"Lichtenstein","year":"1985","journal-title":"Proc. 12th ACM Symp. on Principles of Programming Languages"},{"key":"2026040605562786100_ref061","doi-asserted-by":"crossref","first-page":"196","DOI":"10.1007\/3-540-15648-8_16","article-title":"The glory of the past","volume":"193","author":"Lichtenstein","year":"1985","journal-title":"Logics of Programs"},{"key":"2026040605562786100_ref062","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/3-540-46691-6_8","article-title":"Optimal bounds for the transformation of \u03c9-automa-ta","volume":"1738","author":"L\u00f6ding","year":"1999","journal-title":"Proc. 19th Conf. on Foundations of Software Technology and Theoretical Computer Science"},{"key":"2026040605562786100_ref063","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","author":"Manna","year":"1992","journal-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification"},{"key":"2026040605562786100_ref064","doi-asserted-by":"crossref","first-page":"521","DOI":"10.1016\/S0019-9958(66)80013-X","article-title":"Testing and generating infinite sequences by a finite automaton","volume":"9","author":"McNaughton","journal-title":"Information and Control"},{"key":"2026040605562786100_ref065","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1109\/SWAT.1972.29","article-title":"The equivalence problem for regular expressions with squaring requires exponential space","author":"Meyer","year":"1972","journal-title":"Proc. 13th IEEE Symp. on Switching and Automata Theory"},{"key":"2026040605562786100_ref066","first-page":"1988","article-title":"Complementation is more difficult with automata on infinite words","author":"Michel"},{"issue":"2","key":"2026040605562786100_ref067","first-page":"269","article-title":"Finite-state transducers in language and speech pro-cessing","volume":"23","author":"Mohri","journal-title":"Computational Linguistics"},{"issue":"2","key":"2026040605562786100_ref068","doi-asserted-by":"crossref","first-page":"1045","DOI":"10.1109\/TSMCB.2003.819485","article-title":"Fuzzy branching temporal logic","volume":"34","author":"Moon","journal-title":"IEEE Transactions on Systems, Man, and Cybernetics, Part B"},{"key":"2026040605562786100_ref069","first-page":"100","article-title":"Alternating automata on infinite trees","volume":"192","author":"Muller","year":"1985","journal-title":"Automata on Infinite Words"},{"issue":"3","key":"2026040605562786100_ref070","first-page":"5","article-title":"From nondeterministic B\u00fcchi and Streett automata to deterministic parity automata","volume":"3","author":"Piterman","journal-title":"Logical Methods in Computer Science"},{"key":"2026040605562786100_ref071","first-page":"27","article-title":"Temporal logic and fair discrete systems","volume":"2018","author":"Piterman","journal-title":"Handbook of Model Checking"},{"key":"2026040605562786100_ref072","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1016\/0304-3975(81)90110-9","article-title":"The temporal semantics of concurrent programs","volume":"13","author":"Pnueli","journal-title":"Theoretical Computer Science"},{"key":"2026040605562786100_ref073","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1007\/978-3-540-69850-0_11","article-title":"On the merits of temporal testers","volume":"5000","author":"Pnueli","year":"2008","journal-title":"25 Years of Model Checking"},{"key":"2026040605562786100_ref074","first-page":"337","article-title":"Specification and verification of concur-rent systems in Cesar","volume":"137","author":"Queille","year":"1982","journal-title":"Proc. 8th ACM Symp. on Principles of Programming Languages"},{"key":"2026040605562786100_ref075","first-page":"1","article-title":"Decidability of second order theories and automata on infinite trees","volume":"141","author":"Rabin","journal-title":"Transaction of the AMS"},{"key":"2026040605562786100_ref076","first-page":"595","article-title":"Decidable theories","volume":"1977","author":"Rabin","journal-title":"Handbook of Mathematical Logic"},{"key":"2026040605562786100_ref077","first-page":"115","article-title":"Finite automata and their decision problems","volume":"3","author":"Rabin","journal-title":"IBM Journal of Research and Development"},{"key":"2026040605562786100_ref078","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1109\/SFCS.1988.21948","article-title":"On the complexity of \u03c9-automata","author":"Safra","year":"1988","journal-title":"Proc. 29th IEEE Symp. on Foundations of Computer Science"},{"key":"2026040605562786100_ref079","first-page":"661","article-title":"B\u00fcchi complementation made tight","volume":"3","author":"Schewe","year":"2009","journal-title":"Proc. 26th Symp. on Theoretical Aspects of Computer Science"},{"key":"2026040605562786100_ref080","first-page":"400","article-title":"Beyond Hyper-Minimisation\u2014Minimising DBAs and DPAs is NP-Complete","volume":"8","author":"Schewe","year":"2010","journal-title":"Proc. 30th Conf. on Foundations of Software Technology and Theoretical Computer Science"},{"issue":"1","key":"2026040605562786100_ref081","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1002\/j.1538-7305.1949.tb03624.x","article-title":"The synthesis of two terminal switching circuits","volume":"28","author":"E. Shannon","journal-title":"BELL-SYST-TECH"},{"key":"2026040605562786100_ref082","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","article-title":"The complexity of propositional linear temporal logic","volume":"32","author":"Sistla","journal-title":"Journal of the ACM"},{"key":"2026040605562786100_ref083","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1016\/0304-3975(87)90008-9","article-title":"The complementation prob-lem for B\u00fcchi automata with applications to temporal logic","volume":"49","author":"Sistla","journal-title":"Theoretical Computer Science"},{"key":"2026040605562786100_ref084","doi-asserted-by":"crossref","first-page":"248","DOI":"10.1007\/10722167_21","article-title":"Efficient B\u00fcchi automata from LTL formulae","volume":"1855","author":"Somenzi","year":"2000","journal-title":"Proc. 12th Int. Conf. on Computer Aided Verifica-tion"},{"key":"2026040605562786100_ref085","article-title":"Assertion-based verification","author":"Synopsys","year":"2003"},{"issue":"2","key":"2026040605562786100_ref086","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1137\/0201010","article-title":"Depth first search and linear graph algorithms","volume":"1","author":"Tarjan","journal-title":"SIAM Journal of Computing"},{"key":"2026040605562786100_ref087","first-page":"133","article-title":"Automata on infinite objects","volume":"1990","author":"Thomas","journal-title":"Handbook of The-oretical Computer Science"},{"key":"2026040605562786100_ref088","first-page":"332","article-title":"An automata-theoretic approach to automatic program verification","author":"Vardi","year":"1986","journal-title":"Proc. 1st IEEE Symp. on Logic in Computer Science"},{"issue":"2","key":"2026040605562786100_ref089","first-page":"182","article-title":"Automata-theoretic techniques for modal logics of programs","volume":"32","author":"Vardi","journal-title":"Journal of Computer and Systems Science"},{"issue":"1","key":"2026040605562786100_ref090","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1994.1092","article-title":"Reasoning about infinite computations","volume":"115","author":"Vardi","journal-title":"Information and Computation"},{"key":"2026040605562786100_ref091","doi-asserted-by":"crossref","first-page":"340","DOI":"10.1109\/SFCS.1981.44","article-title":"Temporal logic can be more expressive","author":"Wolper","year":"1981","journal-title":"Proc. 22nd IEEE Symp. on Foundations of Computer Science"},{"key":"2026040605562786100_ref092","first-page":"185","article-title":"Reasoning about infinite computation paths","author":"Wolper","year":"1983","journal-title":"Proc. 24th IEEE Symp. on Foundations of Computer Science"},{"key":"2026040605562786100_ref093","first-page":"589","article-title":"Lower bounds for complementation of \u03c9-automata via the full automata technique","volume":"4052","author":"Yan","year":"2006","journal-title":"Proc. 33rd Int. Colloq. on Au-tomata, Languages, and Programming"}],"container-title":["Foundations and Trends\u00ae in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.emerald.com\/fttcs\/article-pdf\/15\/2\/126\/11150438\/0400000083en.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/www.emerald.com\/fttcs\/article-pdf\/15\/2\/126\/11150438\/0400000083en.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,6]],"date-time":"2026-04-06T09:56:43Z","timestamp":1775469403000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.emerald.com\/fttcs\/article\/15\/2\/126\/1332212\/Multi-Valued-Reasoning-about-Reactive-Systems"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,12,1]]},"references-count":93,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2022,12,1]]}},"URL":"https:\/\/doi.org\/10.1561\/0400000083","relation":{},"ISSN":["1551-305X","1551-3068"],"issn-type":[{"value":"1551-305X","type":"print"},{"value":"1551-3068","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,12,1]]}}}