Muutke küpsiste eelistusi

E-raamat: Advances in Verification of Time Petri Nets and Timed Automata: A Temporal Logic Approach

,
Teised raamatud teemal:
  • Formaat - PDF+DRM
  • Hind: 159,93 €*
  • * 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.
Advances in Verification of Time Petri Nets and Timed Automata: A Temporal Logic ApproachSuurem 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 monograph presents a comprehensive introduction to timed automata (TA) and time Petri nets (TPNs) which belong to the most widely used models of real-time systems. Some of the existing methods of translating time Petri nets to timed automata are presented, with a focus on the translations that correspond to the semantics of time Petri nets, associating clocks with various components of the nets. "Advances in Verification of Time Petri Nets and Timed Automata - A Temporal Logic Approach" introduces timed and untimed temporal specification languages and gives model abstraction methods based on state class approaches for TPNs and on partition refinement for TA. Moreover, the monograph presents a recent progress in the development of two model checking methods, based on either exploiting abstract state spaces or on application of SAT-based symbolic techniques. The book addresses research scientists as well as graduate and PhD students in computer science, logics, and engineering of real time systems.
List of Figures XVII
List of Symbols XXIII
Part I Specifying Timed Systems and Their Properties
1 Petri Nets with Time
3(26)
1.1 Incorporating Time into Petri Nets
6(1)
1.2 Time Petri Nets
7(10)
1.2.1 Distributed Time Petri Nets
8(3)
1.2.2 Semantics: The Clock Approach
11(4)
Clocks Assigned to the Transitions
11(1)
Clocks Assigned to the Places
12(2)
Clocks Assigned to the Processes
14(1)
1.2.3 Semantics: Firing Intervals
15(2)
1.3 Reasoning about Time Petri Nets
17(12)
1.3.1 Comparison of the Semantics
17(1)
1.3.2 Dense versus Discrete Semantics
18(5)
Alternative (Discrete) Semantics
21(2)
1.3.3 Concrete Models for TPNs
23(1)
1.3.4 Progressiveness in Time Petri Nets
23(4)
1.3.5 The Case of "General" TPNs
27(2)
2 Timed Automata
29(22)
2.1 Time Zones
29(4)
2.2 Networks of Timed Automata
33(5)
2.3 Semantics of Timed Automata
38(3)
2.3.1 Alternative (Discrete) Semantics
40(1)
2.4 Concrete Models for TA
41(1)
2.5 Checking Progressiveness
42(9)
2.5.1 A Static Technique
44(2)
2.5.2 Applying Verification Methods
46(2)
2.5.3 A Solution for Strongly Monotonic Semantics
48(3)
3 From Time Petri Nets to Timed Automata
51(12)
3.1 Translations to Extended Timed Automata
51(2)
3.2 Translation for "Clocks Assigned to the Transitions"
53(2)
3.3 Translation for "Clocks Assigned to the Places"
55(8)
3.3.1 Supplementary Algorithms
57(2)
Obtaining General TA
57(1)
Obtaining Diagonal-Free TA
58(1)
3.4 Translation for Distributed Nets
59(3)
3.5 Comparing Expressiveness of TPNs and TA
62(1)
4 Main Formalisms for Expressing Temporal Properties
63(26)
4.1 Non-temporal Logics
63(3)
4.1.1 Propositional Logic (PL)
63(2)
Syntax of PL
63(1)
Semantics of PL
64(1)
4.1.2 Quantified Propositional Logic (QPL)
65(1)
Syntax of QPL
65(1)
Semantics of QPL
65(1)
4.1.3 (Quantified) Separation Logic ((Q)SL)
65(1)
Syntax of (Q)SL
65(1)
Semantics of (Q)SL
66(1)
4.2 Untimed Temporal Logics
66(11)
4.2.1 Computation Tree Logic* (CTL*)
67(4)
Syntax of CTL*
67(1)
Sublogicsof CTL*
67(2)
Semantics of CTL*
69(2)
4.2.2 Modal μ-Calculus
71(3)
Syntax of Modal μ-Calculus
Semantics of Modal mu;-Calculus
79
4.2.3 Interpretation of Temporal Logics over Timed Systems Models
74(3)
4.3 Timed Temporal Logics
77(12)
4.3.1 Timed Computation Tree Logic (TCTL)
75(5)
Syntax of TCTL
75(1)
Semantics of TCTL over Timed Systems
76(1)
Strongly Monotonic Interval Semantics
76(2)
Weakly Monotonic Interval Semantics
78(2)
4.3.2 Timed μ-Calculus (Tμ)
80(2)
Syntax of Tμ
80(1)
Semantics of Tμ
80(2)
4.3.3 Syntax and Semantics of TCTLc
82(7)
Part II Model Generation and Verification
5 Abstract Models
89(66)
5.1 Model Generation for Time Petri Nets
96(19)
5.1.1 State Class Approaches
96(19)
State Class Graph
96(7)
Geometric Region Graph
103(4)
Atomic State Class Graph
107(4)
Pseudo-atomic State Class Graph
111(1)
Strong State Class Graph
112(3)
Strong Atomic State Class Graph
115(1)
5.1.2 Other Approaches – an Overview
115(1)
5.2 Model Generation for Timed Automata
115(31)
5.2.1 Detailed Region Graphs
116(6)
5.2.2 Partition Refinement
122(16)
Bisimulating Models
124(1)
The Algorithm of Bouajjani et al.
124(1)
A Convexity-Preserving Technique
127(1)
The Lee–Yannakakis Algorithm
130(3)
Simulating Models
133(2)
Pseudo-bisimulating Models
135(1)
A Convexity-Preserving Technique
137(1)
Pseudo-simulating Models
137(1)
Other Minimization Techniques
138(1)
5.2.3 Forward-reachability Graphs
138(8)
Abstractions for Forward-reachability Graphs
140(1)
Inclusion Abstraction
140(1)
Extrapolation Abstraction
142(1)
Other Abstractions
145(1)
5.3 Difference Bounds Matrices
146(9)
5.3.1 Operations on Zones Using DBMs
148(7)
Intersection
148(1)
Clock Resets
148(2)
Time Successor
150(1)
Time Predecessor
150(1)
Immediate Time Predecessor
150(3)
Zone Difference
153(2)
6 Explicit Verification
155(26)
6.1 Model Checking for CTL
155(16)
6.1.1 State Labelling
155(3)
6.1.2 Automata-Theoretic Approach
158(13)
Alternating Automata
158(6)
Translation from CTL to WAA
164(2)
Model Checking with WAA
166(1)
Product Automaton
167(3)
Checking Non-emptiness of 1-Letter Word WAA
170(1)
6.2 Model Checking for TCTL over Timed Automata
171(7)
6.2.1 Verification Using Translation from TCTL to CTL
171(7)
Model Checking over Region Graph Models
172(6)
Model Checking over (Bi)simulating Models
178(1)
6.2.2 Overview of Other Approaches to TCTL Verification
178(1)
6.3 Selected Tools
178(3)
6.3.1 Tools for TPNs
179(1)
6.3.2 Tools for TA
179(2)
7 Verification Based on Satisfiability Checking
181(50)
7.1 Bounded Model Checking Using Direct Translation to SAT
182(21)
7.1.1 Discretization of TA
182(9)
Discretized Model for (Un)reachability Verification
185(3)
Discretized Model for TCTL Verification
188(3)
7.1.2 Bounded Model Checking for ECTUr-x
191(10)
7.1.3 Checking Reachability with BMC
201(1)
7.1.4 Checking Unreachability with BMC
201(2)
7.2 Bounded Model Checking via Translation to SL
203(4)
7.2.1 Encoding k-Paths
203(1)
7.2.2 Product Encoding
204(1)
7.2.3 Encoding of LTL Formulas
205(2)
No loop case
205(2)
Loop case
207(1)
7.2.4 Optimizations of the Encoding
207(1)
7.3 Unbounded Model Checking for Tμ
207(5)
7.3.1 From Real to Boolean Quantification
211(1)
7.3.2 From QSL Formulas Without Real-Time Quantification to Equivalent Boolean Formulas
212(1)
7.4 Deciding Separation Logic (MATH-SAT)
212(6)
7.4.1 From SL to Propositional Logic
212(5)
Propositional Encoding
213(1)
Building the Inequality Graph
213(1)
Transitivity Constraints
214(2)
Complexity and Optimization
216(1)
7.4.2 Other Approaches to Deciding SL
217(1)
7.5 Deciding Propositional Formulas (SAT)
218(7)
7.5.1 Boolean Constrain Propagation
220(2)
7.5.2 Conflict-Based Learning
222(2)
7.5.3 Variable Selection (VS)
224(1)
7.6 From a Fragment of QPL to PL
225(4)
7.7 Remaining Symbolic Approaches - Overview
229(1)
7.8 Selected Tools
229(2)
Concluding Remarks and Future Research Directions 231(2)
References 233(12)
Index 245(6)
Author Index 251


Lisainfo e-raamatute kohta Lisainfo e-raamatute kohta
Püsilink: https://www.kriso.ee/db/97835403287042e.html
Märksõnad: