Muutke küpsiste eelistusi

E-raamat: Temporal Logics in Computer Science: Finite-State Systems

4.00/5 (2 hinnangut Goodreads-ist)
(Centre National de la Recherche Scientifique (CNRS), Paris), (Stockholms Universitet), (Universität Kassel, Germany)
Teised raamatud teemal:
  • Formaat - EPUB+DRM
  • Hind: 132,14 €*
  • * hind on lõplik, st. muud allahindlused enam ei rakendu
  • Lisa ostukorvi
  • Lisa soovinimekirja
  • See e-raamat on mõeldud ainult isiklikuks kasutamiseks. E-raamatuid ei saa tagastada.
Temporal Logics in Computer Science: Finite-State SystemsSuurem pilt
Teised raamatud teemal:

DRM piirangud

  • Kopeerimine (copy/paste):

    ei ole lubatud

  • Printimine:

    ei ole lubatud

  • Kasutamine:

    Digitaalõiguste kaitse (DRM)
    Kirjastus on väljastanud selle e-raamatu krüpteeritud kujul, mis tähendab, et selle lugemiseks peate installeerima spetsiaalse tarkvara. Samuti peate looma endale  Adobe ID Rohkem infot siin. E-raamatut saab lugeda 1 kasutaja ning alla laadida kuni 6'de seadmesse (kõik autoriseeritud sama Adobe ID-ga).

    Vajalik tarkvara
    Mobiilsetes seadmetes (telefon või tahvelarvuti) lugemiseks peate installeerima selle tasuta rakenduse: PocketBook Reader (iOS / Android)

    PC või Mac seadmes lugemiseks peate installima Adobe Digital Editionsi (Seeon tasuta rakendus spetsiaalselt e-raamatute lugemiseks. Seda ei tohi segamini ajada Adober Reader'iga, mis tõenäoliselt on juba teie arvutisse installeeritud )

    Seda e-raamatut ei saa lugeda Amazon Kindle's. 

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.

This comprehensive text provides a modern and technically precise exposition of the fundamental theory and applications of temporal logics in computer science. It is a solid professional reference for researchers in the field and a graduate textbook that can be used for self-study as well as for teaching courses.

Arvustused

'In summary, the book presents the most important and influential temporal logics, presents their properties, and introduces the most important tools to reason about temporal logics. It strikes a good balance between breadth and depth in coverage ' Martin Zimmermann, MathSciNet

Muu info

A comprehensive, modern and technically precise exposition of the theory and main applications of temporal logics in computer science.
1 Introduction
1(16)
1.1 Temporal Logics and Computer Science: A Brief Overview
1(5)
1.2 Structure and Summary of the Book Content
6(6)
1.3 Using the Book for Teaching or Self-Study
12(5)
PART I MODELS
2 Preliminaries and Background I
17(18)
2.1 Sets and Relations
18(7)
2.2 Some Fundamental Preliminaries
25(10)
3 Transition Systems
35(50)
3.1 Basic Concepts
37(12)
3.2 Reachability
49(6)
3.3 Bisimulation Relations
55(7)
3.4 Bisimilarity
62(9)
3.5 Trace Equivalence
71(4)
3.6 Exercises
75(4)
3.7 Bibliographical Notes
79(6)
PART II LOGICS
4 Preliminaries and Background II
85(15)
4.1 Preliminaries on Modal Logic
85(6)
4.2 Logical Decision Problems
91(2)
4.3 Expressive Power
93(1)
4.4 Deductive Systems
93(7)
5 Basic Modal Logics
100(50)
5.1 The Basic Modal Logic BML
102(5)
5.2 Renaming and Normal Forms
107(3)
5.3 Modal and Bisimulation Equivalence
110(6)
5.4 Model Checking
116(7)
5.5 Satisfiability and the Tree Model Property
123(8)
5.6 The Basic Tense Logic BTL
131(4)
5.7 Axiomatic Systems
135(6)
5.8 Exercises
5.9 Bibliographical Notes
141(9)
6 Linear-Time Temporal Logics
150(59)
6.1 Syntax and Semantics on Linear Models
152(7)
6.2 Logical Decision Problems
159(5)
6.3 The Small Model Property
164(5)
6.4 Decision Procedures
169(7)
6.5 Adding Past-Time Operators
176(6)
6.6 Invariance Properties
182(3)
6.7 Extensions of LTL
185(6)
6.8 An Axiomatic System for LTL
191(5)
6.9 Exercises
196(10)
6.10 Bibliographical Notes
206(3)
7 Branching-Time Temporal Logics
209(62)
7.1 A Hierarchy of Branching-Time Logics
211(17)
7.2 Bisimulation Invariance
228(5)
7.3 Model Checking
233(8)
7.4 Some Fragments and Extensions of CTL*
241(11)
7.5 Axiomatic Systems
252(7)
7.6 Exercises
259(6)
7.7 Bibliographical Notes
265(6)
8 The Modal Mu-Calculus
271(58)
8.1 Fixpoint Quantifiers
272(10)
8.2 Fixpoint Iteration
282(7)
8.3 The Structural Complexity of Formulae
289(14)
8.4 Model-Checking Games
303(6)
8.5 Bisimulation Invariance
309(4)
8.6 The Second-Order Nature of Temporal Logics
313(2)
8.7 Variants
315(5)
8.8 Exercises
320(4)
8.9 Bibliographical Notes
324(5)
9 Alternating-Time Temporal Logics
329(32)
9.1 Concurrent Multiagent Transition Systems
330(7)
9.2 Temporal Logics for Concurrent Game Models
337(9)
9.3 Logical Decision Problems
346(6)
9.4 Exercises
352(3)
9.5 Bibliographical Notes
355(6)
PART III PROPERTIES
10 Expressiveness
361(58)
10.1 Embeddings among Linear-Time Logics
363(13)
10.2 Embeddings among Branching-Time Logics
376(9)
10.3 Separation Results
385(24)
10.4 Exercises
409(5)
10.5 Bibliographical Notes
414(5)
11 Computational Complexity
419(48)
11.1 Proving Lower Bounds
421(14)
11.2 Linear-Time Temporal Logics
435(10)
11.3 Branching-Time Temporal Logics
445(8)
11.4 An Overview of Completeness Results
453(4)
11.5 Exercises
457(3)
11.6 Bibliographical Notes
460(7)
PART IV METHODS
12 Frameworks for Decision Procedures
467(9)
12.1 A Brief Introduction to Three Methodologies
468(4)
12.2 The Frameworks Compared
472(4)
13 Tableaux-Based Decision Methods
476(67)
13.1 A Generic Incremental Tableau Construction
479(19)
13.2 Tableaux for LTL
498(16)
13.3 Tableaux for TLR and CTL
514(22)
13.4 Exercises
536(4)
13.5 Bibliographical Notes
540(3)
14 The Automata-Based Approach
543(82)
14.1 Introduction to Nondeterministic Buchi Automata
546(6)
14.2 From LTL Formulae to Automata
552(18)
14.3 Introduction to Alternating Automata on Words
570(11)
14.4 From LTL Formulae to Alternating Buchi Automata
581(10)
14.5 Extensions of LTL
591(7)
14.6 Tree Automata for Branching-Time Logics
598(8)
14.7 Alternating Tree Automata and CTL
606(9)
14.8 Exercises
615(6)
14.9 Bibliographical Notes
621(4)
15 The Game-Theoretic Framework
625(91)
15.1 Parity Games
627(20)
15.2 Constructions for Automata on Infinite Words
647(12)
15.3 Model Checking
659(23)
15.4 Satisfiability Checking
682(23)
15.5 Exercises
705(6)
15.6 Bibliographical Notes
711(5)
References 716(21)
Index 737
Stéphane Demri is a CNRS directeur de recherche at the Laboratoire Spécification et Vérification (LSV), Ecole Normale Supérieure de Cachan, and he is currently the head of LSV. His current research interests include verification of infinite-state systems, temporal logics and analysis of systems with data. He has participated in numerous international and national projects and has been co-responsible for bilateral projects with Poland, South Africa and Australia. He is regularly involved in teaching, in program committees, in steering committees and in editorial boards. He has co-authored more than 125 publications in the field of formal/logical methods for analysing computer systems, including a monograph, 4 edited proceedings, 6 book chapters and 50 articles in international journals. Valentin Goranko is currently a professor of logic and theoretical philosophy at Stockholm University. He has more than 30 years of university teaching and research experience in mathematics, computer science and philosophy in universities in Bulgaria, South Africa, Denmark and Sweden. His main expertise and research interests are in theory and applications of modal and temporal logics to computer science, artificial intelligence, multiagent systems and philosophy. He has authored and co-authored more than 100 publications, including two recent textbooks on logic and discrete mathematics. He is a member of several editorial boards and steering bodies of professional organisations and is currently the vice-president of the Association for Logic, Language and Information (FoLLI). Martin Lange is currently a professor in theoretical computer science at the University of Kassel, Germany. His research interests include model checking and general decision procedures for logics in computer science with a focus on temporal logics. He has published more than 80 papers in international journals and conference proceedings. He received an ERC Starting Grant in 2010 and a Heisenberg professorship from the German Research Council in 2013.
Lisainfo e-raamatute kohta Lisainfo e-raamatute kohta
Püsilink: https://www.kriso.ee/db/97813167271646e.html