Formal Methods in Computer Science

✍ Scribed by Jiacun Wang, William Tepfenhart

• Publisher: CRC Press
• Year: 2020
• Tongue: English
• Leaves: 314
• Series: Textbooks in Mathematics
• Category: Library

✦ Table of Contents

Contents
Taylor &. Francis
Preface
Book Layout
Audience
Jiacun Wang, PhD
Taylor &. Francis
Acknowledgments
Taylor &. Francis
Authors
Taylor &. Francis
1
Set Theory and Functions
1.1 Basic Set Definitions
1.2 Set Operations
1.2.1 Union
1.2.2 Intersection
1.2.3 Set Difference
A\A = 0
A\0 = A
C(C\A)
(C о A) и (C\C)
(B\A) о C = (B о C)\A = B о (C\A)
(B\A) и C = (B и C)(A\C)
A A B = (A\B) о (B\A) Definition
(B\A) о (A\B) Union is communitive (1.43)
BA A Definition
A A 0 = (A\0) и (0\A) Definition
1.2.4 Power Set
1.3 Ordered Pairs
1.4 Relations
1.5 Functions
1.5.1 Partial Functions
1.5.2 Into/Onto
1.5.3 Composition
Exercises
2
Finite State Machine
2.1 Key Concepts of Finite State Machines
2.2 Accepting States
2.3 State Machines with Output
2.3.1 Mealy
2.3.2 Moore
2.3.3 Harel (UML)
State Machine Ceiling Fan
Exercises
3
Regular Expressions and Languages
3.1 Strings and Languages
3.2 Regular Expressions
3.3 Lex
3.4 Grammar
3.4.1 Productions
3.4.2 Derivations
3.4.3 Parse Trees
3.4.4 Removing Left Recursion
3.4.5 Left Factoring
3.5 Regular Expressions versus Grammars
Exercises
4
Propositional Logic
4.1 Propositional Statements
4.2 Logic Operators and Truth Tables
4.2.1 Well-Formed Formulas
4.2.2 Truth Values
4.2.3 Evaluation of Propositional Formulas
4.3 Logic Equivalencies
4.4 Logic Arguments
4.4.1 Validity and Soundness
4.4.2 Validity Test through Truth Tables
4.4.3 Inference Rules
premise 1, premise 2, ..., premise m
4.5 Satisfiability of Formulas
4.5.1 Conjunctive Normal Forms
4.5.2 Horn Clauses
Exercises
5
Predicate Logic
5.1 Predicates
5.2 Quantifiers
5.2.1 Universal Quantifier
5.2.2 Existential Quantifier
5.2.3 Properties of Quantifiers
5.3 Syntax of Predicate Logic
5.3.1 Terms
5.3.2 Formulas
5.3.3 Parse Trees
5.3.4 Free and Bound Variables
5.3.5 Substitution
5.4 Natural Deduction Rules
5.4.1 Rules for Equality
5.4.2 Rules for Universal Quantifier
5.4.3 Rules for the Existential Quantifier
5.5 Semantics of Predicate Logic
5.5.1 Interpretation and Models
5.5.2 Evaluation of Truth Values
5.5.3 Satisfiability and Validity
Exercises
Taylor &. Francis
6
Temporal Logic
6.1 Temporal Logic
6.1.1 Kripke Structures
6.1.2 Modeling of Time
6.2 Linear Temporal Logic
6.2.1 Syntax of LTL
9 ::= T 11 p\ (-9 ) I (9 A 9 ) | (9 V 9 ) I (9 ^ 9 )
(6.1) (X9) (F9) | (g9)|(9u9) | (9R9)
6.2.2 Parse Trees of LTL Formulas
6.2.3 Semantics of LTL
6.2.4 Equivalencies of LTL Formulas
6.2.5 System Property Specification
6.3 Computation Tree Logic
6.3.1 Syntax of CTL
V ::=ТШ p I (-y) I (ф л y) I (y v y) I (y ^ y)
I(AXp)I(EXф) I(AGo)I(EGp)I(AFo)I(EFp) (6.2)
I A(^Uф)\ E(^U^)
6.3.2 Semantics of CTL
6.3.3 Equivalencies of CTL Formulas
6.3.4 System Property Specification
6.3.5 LTL versus CTL
6.4 CTL
Ф ::= Т |1 \р\ (-р) | (ф л р) | (ф v ф) | (ф ^ р) (A) \ (E *)
V ::= pl (-V) I (y ay) I (y vy) I (y ^ y)
|Xy)|Gy)|Fy|yUy
Exercises
Taylor &. Francis
7
Formal Verification by Model Checking
7.1 Introduction to Model Checking
7.2 CTL Model Checking Algorithm
7.2.1 The Labeling Algorithm
7.2.2 State Explosion Issues in Model Checking
7.3 The NuSMV Model Checking Tool
7.3.2 Specifications
7.3.3 Running NuSMV
7.4 Example: The Ferryman Puzzle
Exercises
8
Petri Nets
8.1 Petri Nets
8.1.1 Multiplicity of Arcs
8.2 Common Petri Net Structures and Substructures
8.2.1 Sequential Execution
8.2.2 Concurrent Execution
8.2.3 Synchronization
8.2.4 Nondeterminism
8.2.5 Loop
8.2.6 Source
8.2.7 Consumer
8.2.8 Control
8.2.9 Accumulator
8.3 Reduction Rules
8.3.1 Fusion of Series Places
8.3.2 Fusion of Series Transitions
8.3.3 Fusion of Parallel Places
8.3.4 Fusion of Parallel Transitions
8.3.5 Elimination of Self-Loop Places
8.3.6 Elimination of Self-Loop Transitions
8.4 Modeling
8.5 Mathematical Description of Petri Nets
8.6 Petri Net Behavior
8.6.1 Reachability
8.6.2 Boundedness
8.6.3 Liveness
8.6.4 Reversibility
8.6.5 Fairness
8.6.6 Incidence Matrix
8.6.7 T-Invariants
8.6.8 S-Invariants
8.6.9 Siphons and Traps
Exercises
Taylor &. Francis
9
Timed Petri Nets
9.1 Introducing Time to Petri Nets
9.2 Deterministic Timed Petri Nets
9.2.1 States in DTPNs
9.2.2 Transition Firing Rules
9.2.3 Performance Evaluation Based on DTPNs
s i- Si (n) Ci = lim ——L
= CN
C = maxfT^ I k = 1,2, .^, q} Nk
9.3 Probability and Stochastic Process
9.3.1 Probability
Fx (x ) = Pr {X < x}
lim FX (x)= 1
Pr {A, B} Pr {B}
9.3.2 Stochastic Process
9.3.3 Continuous-Time Markov Chains
9.4 Stochastic Petri Nets
9.4.1 Definition
T = {t e E (Mi )| Mi [ t > Mj}
9.4.2 Performance Evaluation
Exercises
-1
1
-3 0
-1
-2
-2
-1
1
-5
0
-2
2
-2
1
-5
10
Colored Petri Nets
10.1 Introductory Examples
10.2 Colored Petri Nets
10.2.1 Multi-Set
10.2.2 Variable Set of an Expression
10.2.3 Evaluation of an Expression
10.3 Analysis of Colored Petri Nets
Exercises
Taylor &. Francis
Index