- Oggetto:
The ULTraS Framework: New Behavioral Equivalences for Nondeterministic and Probabilistic Processes and Their Spectrum
- Oggetto:
Academic year 2013/2014
- Course ID
- SEM-ULTRAS
- Year
- 1° anno 2° anno 3° anno
- Teaching period
- Seminario
- Type
- Seminario
- Credits/Recognition
- 0
- Course disciplinary sector (SSD)
- INF/01 - informatica
- Delivery
- Tradizionale
- Language
- Inglese
- Attendance
- Facoltativa
- Type of examination
- Non prevista
- Oggetto:
Sommario del corso
- Oggetto:
Course objectives
Labeled transition systems are typically used as behavioral models of concurrent processes. Their labeled transitions define a one-step state-to-state reachability relation. This model can be generalized by
modifying the transition relation to associate a state reachability distribution with any pair consisting of a source state and a transition label. The state reachability distribution is a function mapping each possible target state to a value that expresses the degree of one-step reachability of that state. Values are taken from a preordered set equipped with a minimum that denotes unreachability. By selecting suitable preordered sets, the resulting model, called ULTraS from Uniform Labeled TRAnsition System, can be specialized to capture well-known models of fully nondeterministic processes (LTS), fully probabilistic processes (ADTMC), fully stochastic processes (ACTMC), and nondeterministic and probabilistic (MDP) or nondeterministic and stochastic (CTMDP) mixed processes. This uniform treatment of different behavioral models extends to behavioral equivalences. They can be defined on ULTraS by relying on appropriate measure functions that express the degree of reachability of a set of states when performing multi-step computations. It is shown that the specializations of bisimulation, trace, and testing equivalences for the
different classes of ULTraS coincide with the behavioral equivalences defined in the literature over traditional models except when nondeterminism and probability/stochasticity coexist; then new equivalences pop up.
Suggested readings and bibliography
- Oggetto:
Class schedule
Days Time Classroom Martedì 9:30 - 11:00 Sala Seminari Dipartimento di Informatica Lessons: dal 26/02/2013 to 26/02/2013
- Oggetto:
Note
The seminar will be held by
prof. Marco Bernardo
Universita' di Urbino
- Oggetto: