Martin Lange

This comprehensive text provides a modern and technically precise exposition of the fundamental theory and applications of temporal logics in computer science. Part I presents the basics of discrete transition systems, including constructions and behavioural equivalences. Part II examines the most important temporal logics for transition systems and Part III looks at their expressiveness and complexity. Finally, Part IV describes the main computational methods and decision procedures for model checking and model building - based on tableaux, automata and games - and discusses their relationships. The book contains a wealth of examples and exercises, as well as an extensive annotated bibliography. Thus, the book is not only a solid professional reference for researchers in the field but also a comprehensive graduate textbook that can be used for self-study as well as for teaching courses.

Inhaltlich unver nderte Neuauflage. Martin Lange hat es sich zum Ziel gesetzt, sowohl die Ursachen des demografischen Wandels darzulegen als auch die Verhaltensdispositionen lterer Mitarbeiter insoweit zu erfassen, dass die "berufsbezogenen Leistungs-motiva-tionen" gemessen und interpretiert werden. Hierbei geht er aus unterschiedlichen Blickrichtungen der Kernfrage nach, ob es Unterschiede zwischen der Leistungsmotivation j ngerer und lterer Arbeit-nehmer gibt. Bestehen Unterschiede in der Leistungsmotivation von lteren Arbeitnehmern mit und ohne F hrungsverantwortung? Beeintr chtigt es das Eigenbild und die Leistungsmotivation lterer Mitarbeiter, wenn ihnen von dritter Seite fehlende Leistungsf higkeit suggeriert wird? Nehmen ltere Arbeit-nehmer Motivationsbarrieren st rker wahr als ihre j ngeren Kollegen? Um Antworten auf diese und andere Fragen zu erhalten, f hrte Martin Lange im Jahr 2006 eine explorative Befragung in Beh rden und diversen Wirtschaftsunternehmen durch.

Das Buch beschäftigt sich mit der Theorie endlicher Automaten auf endlichen und unendlichen Wörtern sowie Bäumen. Es behandelt klassische Resultate wie die Sätze von Büchi und Rabin, die zeigen, wie sich monadische Logiken 2. Stufe auf diesen Strukturen mithilfe dieser Automatentheorie entscheiden lassen. Die einzelnen Kapitel sind in vier Teile zusammengefasst. Diese unterscheiden sich in den Strukturen, über denen jeweils Automatentheorie und Logik betrieben wird. Der erste Teil behandelt endliche Wörter. Der Zweite die Theorie auf den Bereich der Bäume auszudehnen. Der dritte Teil beschäftigt sich kurz mit endlichen Bäumen. Im vierten Teil geht es dann um Automatentheorie und Logik über unendliche Bäume. Jeder Teil endet mit Vorschlägen für Übungsaufgaben zu dem behandelten Stoff, sowie Notizen, welche auf weiterführende Literatur verweisen oder die Herkunft von präsentierten Resultaten erklären. Das Buch ist an sich ein geschlossenes Werk, welches mit den bereits erwähnten Vorkenntnissen zur Theorie formaler Sprachen und zunächst ohne weitere Hilfsmittel durchgearbeitet werden kann.