From Monadic Logic to PSL

One of the surprising developments in the area of program verification is how ideas introduced originally by logicians in the 1950s ended up yielding by 2003 an industrial-standard property-specification language called PSL. This development was enabled by the equally unlikely transformation of the mathematical machinery of automata on infinite words, introduced in the early 1960s for second-order arithmetics, into effective algorithms for model-checking tools. This paper attempts to trace the tangled threads of this development. 1 Thread I: Classical Logic of Time

• Type: Conference
• Year: 2008
• Where: BIRTHDAY
• Authors: Moshe Y. Vardi
• Keywords: Applied Computing, BIRTHDAY 2008, Language Called Psl, Second-order Arithmetics, Surprising Developments