caa a22 4500 467989850 CHVBK 20180323112541.0 cr unu---uuuuu 170328e19900901xx s 000 0 eng 10.1007/BF00264284 doi (NATIONALLICENCE)springer-10.1007/BF00264284 Cleaveland Rance Department of Computer Science, North Carolina State University, Box 8206, 27695-8206, Raleigh, NC, USA aut Tableau-based model checking in the propositional mu-calculus [Elektronische Daten] [Rance Cleaveland] Summary: This paper describes a procedure, based around the construction of tableau proofs, for determining whether finite-state systems enjoy properties formulated in the propositional mu-calculus. It presents a tableau-based proof system for the logic and proves it sound and complete, and it discusses techniques for the efficient construction of proofs that states enjoy properties expressed in the logic. The approach is the basis of an ongoing implementation of a model checker in the Concurrency Workbench, an automated tool for the analysis of concurrent systems. Springer-Verlag, 1990 Acta Informatica Springer-Verlag 27/8(1990-09-01), 725-747 0001-5903 27:8<725 1990 27 236 https://doi.org/10.1007/BF00264284 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1007/BF00264284 text/html Onlinezugriff via DOI NATIONALLICENCE 100 1- Cleaveland Rance Department of Computer Science, North Carolina State University, Box 8206, 27695-8206, Raleigh, NC, USA aut NATIONALLICENCE 773 0- Acta Informatica Springer-Verlag 27/8(1990-09-01), 725-747 0001-5903 27:8<725 1990 27 236 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer