Video
Not enough ratings.
Modeling Concurrent Systems & Temporal Logics
Create Note
Dear user,
with the manuscript function you'll be able to create your own digital lecture manuscript.
However, in order to link all your notes with your user profile it is required that you
login to the tele-TASK portal to use this functionality.
If you don't have an account yet, you may register for a tele-TASK account here.
with the manuscript function you'll be able to create your own digital lecture manuscript.
However, in order to link all your notes with your user profile it is required that you
login to the tele-TASK portal to use this functionality.
If you don't have an account yet, you may register for a tele-TASK account here.
Add a New Marker
Dear user,
with the marker function you'll be able to create your own digital time markers.
However, in order to link all your markers with your user profile it is required that you
login to the tele-TASK portal to use this functionality.
If you don't have an account yet, you may register for a tele-TASK account here.
with the marker function you'll be able to create your own digital time markers.
However, in order to link all your markers with your user profile it is required that you
login to the tele-TASK portal to use this functionality.
If you don't have an account yet, you may register for a tele-TASK account here.
Tag this content
Please enable javascript to use this function.
Dear user,with the tagging function you'll be able to add taggs to videos.
However, in order to link all your tags with your user profile it is required that you
login to the tele-TASK portal to use this functionality.
If you don't have an account yet, you may register for a tele-TASK account here.
Tags added to this content
No tags have been added to this content so far.
Add Link to this content
Please enable javascript to use this function.
Dear user,with the links function you'll be able to add links to other resources to this content.
However, in order to link all your links with your user profile it is required that you
login to the tele-TASK portal to use this functionality.
If you don't have an account yet, you may register for a tele-TASK account here.
Links added to this content
No links have been added to this content so far.
Add to my playlist
Dear user,
with the playlist function you'll be able to create your own lecture video playlists.
However, in order to link all your playlists with your user profile it is required that you
login to the tele-TASK portal to use this functionality.
If you don't have an account yet, you may register for a tele-TASK account here.
with the playlist function you'll be able to create your own lecture video playlists.
However, in order to link all your playlists with your user profile it is required that you
login to the tele-TASK portal to use this functionality.
If you don't have an account yet, you may register for a tele-TASK account here.
Playlists
This content is not used in any playlist.
1106110111112117165223724726785835836878113413011369152418661946207320742193219521962197222924152490254925652572265926602685296731523170327833673430349735923649376437663818411941294131413244994612461446154667474147434745494550035183525153325427553156055606
Lecture Structure
- Translational Semantics (00:00:01)
- Translational Semantics Mapping Decisions Decisions mapped to XOR split in the (00:01:46)
- Translational Semantics Mapping Initial Marking (00:01:50)
- Operational Semantics (00:01:57)
- Discussion (00:03:43)
- Detailed Outline (00:12:04)
- Discussion (00:12:06)
- Detailed Outline (00:13:05)
- Outline (00:13:55)
- 2 Modeling Concurrent Systems (00:13:56)
- Motivation and Idea (00:14:38)
- Methods Overview (00:18:54)
- Usage (00:21:41)
- Value of model checking in particular (00:21:41)
- Validation (00:18:54)
- ls performed on a systems design (00:18:54)
- and allows observation (00:18:54)
- Testing (00:18:54)
- Test results are investigated to (00:18:54)
- detect errors (00:18:54)
- Petri Net (00:25:24)
- State Space in Concurrent Systems (00:31:07)
- Modeling Systems (00:32:26)
- State Space in Concurrent Systems (00:34:33)
- Petri Net (00:34:34)
- State Space in Concurrent Systems (00:36:33)
- Modeling Systems (00:36:35)
- Structures (00:36:36)
- A structure consists set of states a set of state (00:36:36)
- properties that are true in the state (00:36:36)
- Properties are based on atomic propositions (00:36:36)
- Paths in structures represent computations (00:36:36)
- Modeling Systems (00:36:37)
- Structures (00:37:09)
- Receive (00:40:15)
- Structures (00:41:30)
- Definition Structure (00:42:51)
- Definition Structure (00:44:19)
- 1k f Invoice (00:44:20)
- Definition Structure (00:44:45)
- Definition of Path (00:50:35)
- Path in Structure (00:52:32)
- Valuations and States (00:52:50)
- es over a D a finite set of values (00:52:50)
- A for V is a that maps each (00:52:50)
- 1 E V to a value ill D (00:52:50)
- Example (00:54:38)
- Formulas represent sets of states (00:57:10)
- We can then describe a set of states by one formula (00:57:10)
- Sets of initial states can be described by Q (00:57:10)
- In the example (00:57:10)
- State transitions (00:58:17)
- Example (00:59:52)
- Derive Structure (01:00:49)
- Example (01:02:44)
- Derive Structure (01:02:46)
- Example (01:08:38)
- 3 Temporal Logics (01:08:49)
- Example (01:08:51)
- 3 Temporal Logics (01:14:58)
- Temporal logic is about properties of states and their transitions (01:14:59)
- Let AP be a set of atomic propositions Each element in AP is a state formula (01:16:52)
- Paths in transition systems are investigated Paths are since time does not stop (01:16:54)
- Let AP be a set of atomic propositions Each element in AP is a state (01:16:55)
- Paths in transition systems are investigated Paths are since time does not stop (01:17:47)
- We are interested in different kinds of properties Those that hold for all possible continuations examples (01:19:01)
- Temporal Logic (01:19:03)
- We are interested in different kinds of properties Those that hold for all possible continuations examples (01:19:05)
- Temporal Logic (01:22:26)
- Syntax of (01:23:23)
- Semantics of Temporal Operators (01:26:23)
- Semantics of formally (01:27:31)
- holds ill the state S in the structure A 1 (01:28:52)
- Example (01:30:27)
- Definition of I Relation (01:33:24)
- Definition of Relation (01:33:25)
Keyword
Please enable javascript to use this function.
Please enable javascript to use this function.