| Program |
| Monday 6 |
Tutorial Session: M.1
Validation and Evaluation:
Properties and
Bounds |
| 09h00: |
Marta Kwiatkowska (University of Birmingham, U.K.)
Model checking of probabilistic systems against temporal logic specifications
|
| 10h30: |
Coffee break
|
| 11h00: |
Pierpaolo Degano, Corrado Priami (Univ. di Verona e Pisa, Italy)
Performance evaluation of mobile computations
|
| 12h30: |
--
|
| 13h00: |
Lunch
|
| 14h30: |
Mauro Pezzé (Politecnico di Milano, Italy)
Timed Petri nets
|
| 16h00: |
Coffee break
|
| 16h30: |
Javier Campos (Universidad de Zaragoza, Spain)
Properties and bounds on P/T nets
|
| 18h00: |
--
|
Tutorial Session:M.2
Solution and Analysis of
Large Markov
Chains |
| 09h00: |
Tugrul Dayar (Bilkent University, Turkey)
Introduction to the numerical solution of Markov chains
|
| 10h30: |
Coffee break
|
| 11h00: |
Boudewjin Haverkort (University of Aachen, Germany)
Solution of infinite Markov chains
|
| 12h30: |
--
|
| 13h00: |
Lunch
|
| 14h30: |
Brigitte Plateau (Université de Grenoble, France)
Stochastic automata networks and Kronecker algebra
|
| 16h00: |
Coffee break
|
| 16h30: |
Gianfranco Ciardo (College of William and Mary, USA)
Efficient data structures and algorithms for the Kronecker approach
|
| 18h00: |
--
|
| Workshop On Formal Methods And
Manufacturing |
| 08h45: |
Opening Session
|
| 09h00: |
R. Champagnat, R. Valette, H. Pingaud (LASS/LGC Toulouse, France)
Formal methods for batch production systems
|
| 10h00: |
G. Hetreux, C. Artigues, B. Palomino (ENSIGC Toulouse, LAIL Lille)
A two phase method for short term scheduling in batch processes
|
| 10h30: |
Coffee break
|
| 11h00: |
F. Balduzzi, A. Giua, C. Seatzu (Polit. Torino/ U. Cagliari, Italy)
Modelling automated manufacturing systems with hybrid automata
|
| 11h30: |
I. Demongodin, M. Mostefaoui, N. Sauer (Ecole des Mines de Nantes, France)
Liveness of hybrid marked graphs
|
| 12h00: |
L. Pietrac, B. Denis, J-J. Lesage (INSA-Lyon/ENS de Cachan, France)
An approach of formal meta-modeling for the design methods of automated
manufacturing systems
|
| 12h30: |
--
|
| 13h00: |
Lunch
|
| 14h30: |
S. Kowaleski (U. of Dortmund, Germany)
Formal methods and the processing industries: status and prospects from an
academic perspective
|
| 15h30: |
B.C Damasceno, X. Xie (Inria Metz, France)
Integration of scheduling and deadlock avoidance of manufacturing systems
|
| 16h00: |
Coffee break
|
| 16h30: |
E. Canuto, F. Balduzzi (Politecnico di Torino, Italy)
Manufacturing algebra: a formal method for modelling manufacturing systems
|
| 17h00: |
C. Haro, P. Martineau, C. Proust (E3I, Université de Tours, France)
A new generalized Petri net transformation
|
| 17h30: |
F. Basile, P. Chiacchio, V. Vittorini, Mazzocca (U. di Napoli I and II, Italy)
Modelling flexible manufacturing systems: a Petri net modular approach
|
| 18h00: |
--
|
| Tuesday 7 |
Tutorial Session: T.1
Composition and Decomposition
Methods |
| 09h00: |
Ed Brinksma, Holger Hermanns (Univ. of Twente, The Netherlands)
Advances in Markovian and non Markovian process algebras
|
| 10h30: |
Coffee break
|
| 11h00: |
Claude Dutheillet (Université Paris 6, France)
Automatic exploitation of symmetries with SWNs
|
| 12h30: |
--
|
| 13h00: |
Lunch
|
| 14h30: |
Manuel Silva (Universidad de Zaragoza, Spain)
Net-driven decomposition techniques
|
| 16h00: |
--
|
Tutorial Session: T.2
Analysis of Non Markovian Petri
Nets |
| 09h00: |
Christoph Lindemann (University of Dortmund, Germany)
Deterministic stochastic Petri nets
|
| 10h30: |
Coffee break
|
| 11h00: |
Reinhard German (Technical University of Berlin, Germany)
Numerical analysis of non-Markovian stochastic Petri nets
|
| 12h30: |
--
|
| 13h00: |
Lunch
|
| 14h30: |
Susanna Donatelli (Univ. di Torino, Italy), Patrice Moreaux (Univ. de
Reims, France)
Structured solution methods for GSPN with phase type distributions
|
| 16h00: |
--
|
| Workshop On Formal Methods And
Telecommunications |
| 09h00: |
Opening Session (Chair: Marco Ajmone Marsan, Tomás Robles)
|
| 09h15: |
SDL (Chair: Tomás Robles)
- J.Hintelmann (University of Essen, Germany)
SDL based load and performance models for the design process of
distributed systems
- J.R. Vidal, L. Guijarro, V. Pla, J. Martínez (Univ. Politécnica
de Valencia, Spain)
An SDL modelling approach for performance evaluation of ATM networks
|
| 10h30: |
Coffee break
|
| 11h00: |
Case Studies (Chair: Marco Ajmone Marsan)
- R. Khoussainov, A. Patel
Formal modelling in embedded system design: a case study
- S.Heymer, J.Grabowski (Medical University of Lubeck, Germany)
Chemistry in action: discovering the behaviour of a network from
local observations
- M. Ionescu, A. Cavalli, (Institud National del Telecommunications, France)
Embedded testing for the MAP-CSM protocol
|
| 12h30: |
--
|
| 13h00: |
Lunch
|
| 14h30: |
LOTOS (Chair: Tomás Robles)
- G. Huecas, T. Robles (Univ. Politécnica de Madrid, Spain)
L.F. Llana-Diaz, A. Verdejo (Universidad Complutense de Madrid, Spain)
E-LOTOS: an overview
- C. Shankland (University of Stirling, UK)
A. Verdejo (U. Complutense de Madrid, Spain)
Time, E-LOTOS, and the firewire
|
| 16h00: |
Coffee break
|
| 16h30: |
Petri Nets (Chair: Marco Ajmone Marsan)
- B. Haverkort, A. Ost (Rheinish-Westfalishe Technische Hochschule,
Aachen, Germany)
Experiences in using infinite-state SPNs for modelling communication
systems under self-similar traffic
- M. Ajmone Marsan, R. Gaeta (Politecnico di Torino, Italy)
GSPN and SWN models for ATM
|
| 17h45: |
--
|
Multiworkshop on:
Petri Nets and Performance Models,
Numerical Solutions of Markov Chains
and
Process Algebra and Performance Modelling
|
| Wednesday 8 |
| 09h00: |
Opening Session
|
| 09h30: |
William H. Sanders (Invited-PNPM/University of Illinois, Champaign, U.S.A.):
Integrated frameworks for multi-level and multi-formalism modeling
|
| 10h30: |
Coffee break
|
| Track: W.1 |
| 11h00: |
PN1: Techniques I (Chair: Marco Ajmone Marsan)
- F. G. Vallés, J. M. Colom (Universidad de Zaragoza, Spain)
Implicit places in net systems
- E. Teruel (Univ. Zaragoza, Spain)
G. Franceschinis (Univ. Piemonte Orientale "Amadeo Avogadro", Italy)
M. De Pierro (Univ. Torino, Italy)
Clarifying the priority specification of GSPN: detached priorities
- D. Deavours, W. Sanders (University of Illinois, USA)
An efficient well-specified check
|
| 12h30: |
--
|
| 13h00: |
Lunch
|
| 14h30: |
PN2: Applications to Telecommunication(Chair: Boudewijn Haverkort)
- R. German, A. Heindl (TU Berlin, Germany)
Performance evaluation of IEEE 802.11 wireless LANs with stochastic
Petri nets
- M. Meo, M. Ajmone Marsan (Politecnico di Torino, Italy)
M. Sereno (Univ. di Torino, Italy)
GSPN analysis of dual-band mobile telephony networks
|
| 15h30: |
Coffee Break
|
| 16h00: |
PN3: Non-Markovian Nets (Chair: Alessandro Giua)
- R. German (TU Berlin, Germany)
M. Telek (Tech. University of Budapest, Hungary)
Formal relation of Markov renewal theory and supplementary variable in the
analysis of stochastic Petri nets
- M. Gribaudo, M. Sereno (Univ. di Torino, Italy)
A. Bobbio (Univ. Piemonte Orientale "Amadeo Avogadro", Italy)
Fluid stochastic Petri nets: an extended formalism to include
non-Markovian models
- A. Bobbio (Univ. Piemonte Orientale "Amadeo Avogadro", Italy)
S. Garg (Lucent Techn., USA)
M. Gribaudo, M. Sereno (Univ. di Torino, Italy)
A. Horvarth, M. Telek (Tech. University of Budapest, Hungary)
Modeling software systems with rejuvenation, restoration and
checkpointing through fluid stochastic Petri nets
|
| 17h30: |
Tools session (Chair: Gianfranco Ciardo)
- Peter Buchholz (TU Dresden)
Peter Kemper (Unversitat Dortmund)
Numerical analysis techniques in the APNN toolbox
- Armin Zimmermann, Reinhard German, Jorn Freiheit, Gunter Hommel
(TU Berlin)
TimeNET 3.0 tool description
- Gianfranco Ciardo, Andrew S. Miner (College of William and Mary)
SMART - simulation and Markovian analyzer for reliability and
timing
- Graham Clark, Stephen Gilmore, Jane Hillston (University of Edinburgh)
The PEPA performance modelling tools
- Jean-Claude Hochon, Veronique Font (IXI, Toulouse)
MISS-RdP interactive system modeling and simulation, performance
evaluation by stochastic, colored and hybrid Petri nets
|
| 18h30: |
--
|
| 18h45: |
Reception
|
| Track: W.2 |
| 11h00: |
MC1: Infinite Markov Chains (Chair: William J. Stewart)
- R. Sadre, Boudewijn Haverkort, A. Ost (Rheinish-Westfalishe
Technische Hochschule, Aachen, Germany)
An efficient and accurate decomposition method for open finite and
infinite buffer queueing networks
- G. Ciardo, A. Riska, E. Smirni (College of William and Mary,
Williamsburg, USA)
An aggregation-based solution method for M/G/1-type processes
- I. Adan, J. Resing (Eidhoven University of Technology, The Netherlands)
A class of Markov processes on a semi-infinite strip
|
| 12h30: |
--
|
| 13h00: |
Lunch
|
| 14h30: |
PA1: Non-Markovian SPA (Chair: Jane Hillston)
- A. El-Rayes, M. Kwiatkowska, G. Norman (University of
Birmingham, UK)
Solving infinite stochastic process algebra models through
matrix-geometric methods
- G. Clark (University of Edinburgh, UK)
Stochastic process algebra structure for insensitivity
|
| 15h30: |
Coffee Break
|
| 16h00: |
MC2: Distributed and Parallel Solutions (Chair: Brigitte Plateau)
- W. Knottenbelt, P. Harrison (Imperial College, London, UK)
Distributed disk-based solution techniques for large Markov
models
- P. Buchholz, M. Fischer, P. Kemper (Universitat Dortmund, Germany)
Distributed steady state analysis using Kronecker algebra
- V. Migallon, J. Penades (Universidad de Alicante, Spain)
D. Szyld (Temple University, Philadelphia, USA)
Experimental study of parallel iterative solution of Markov chains
with block partitions
|
| 17h30: |
MCP: Poster Session (Chair: Brigitte Plateau)
- J.M. Fourneau (Université de Versailles Saint Quentin, France)
Stochastic automata networks: using structural properties to reduce
the state space
- M. Jarraya, D. El Baz (LAAS, Toulouse, France)
Asynchronous iterations for the solution of Markov systems
- F. Quessette, A. Troubnikoff (Université de Versailles Saint
Quentin, France)
Using of non-symmetric permutations to solve large Markov
models
- D. Twigg, A. Ramesh, U. Sandadi, A. Anand, C. Sharma (The Boeing
Company, USA)
Reliability computation of systems that operate multiple phases and
multiple missions
|
| 18h30: |
--
|
| 18h45: |
Reception
|
| Thursday 9 |
| 09h00: |
Marcel Neuts (Invited-NSMC/University of Arizona, U.S.A.)
Some recent new problems and results in matrix-analytic methods
|
| Track: T.1 |
| 10h00: |
PN4 (Chair: Alois Ferscha)
- W. Zuberek (Memorial University of Nfld, Canada)
Stepwise refinements of net models and their place invariants
|
| 10h30: |
Coffee break
|
| 11h00: |
PN5: Techniques II (Chair: Peter Kemper)
- B. Haverkort, H. Bohnenkamp, A. Bell (RWTH Aachen, Germany)
On the efficient sequential and distributed evaluation of very large
stochastic Petri nets
- G. Ciardo, A. Miner (College of William and Mary, USA)
A data structure for the efficient Kronecker solution of GSPNs
- C. J. Pérez-Jiménez, J. Campos (Universidad de Zaragoza, Spain)
On state space decomposition for the numerical analysis of
stochastic Petri nets
|
| 12h30: |
--
|
| 13h00: |
Lunch
|
| 14h30: |
PN6: Formalisms (Chair: Javier Campos)
- P. Kemper (Universitaet Dortmund, Germany)
A mapping of autonomous net condition event systems to GSPNs
- R. Gaeta (Univ. di Torino, Italy)
A. Bobbio, G. Franceschinis, L. Portinale (Univ. Piemonte Orientale
"Amadeo Avogadro", Italy)
Exploiting Petri nets to support fault tree based dependability
analysis
|
| 15h30: |
Coffee Break
|
| 16h00: |
Max/Plus (Organiser: E. Wagneur)
- S. Gaubert (INRIA, Domaine de Volueau, France)
J. Mairesse (CNRS- Université, France)
Performance evaluation of timed Petri nets using heaps of
pieces
- S. Lahaye, J. L. Boimond, L. Hardouin (LISA, Univ. Angers, France)
Optimal control of (min, +) linear time-varying systems
- I. Demongodin, E. Wagneur (IRCYN, CNRS, E. Mines de Nantes, France)
On the rational use of Petri nets, automata and the max-plus algebra
for the optimal control of DEDS
|
| 17h30: |
--
|
| Track: T.2 |
| 10h00: |
MC3: Modelling techniques
- R. German (Teschnische Universitat Berlin, Germany)
Cascaded deterministic and stochastic Petri nets
|
| 10h30: |
Coffee break
|
| 11h00: |
MC4: Computational and storage Issues (Chair: Tugrul Dayar)
- I. Sonin, J. Thornton (UNC Charlotte, USA)
Computational properties of algorithm "REFUND" for the
fundamental/group inverse matrix of a Markov chain
- P. Buchholz (Universitat Dortmund, Germany)
Projection methods for the analysis of stochastic automata networks
- S. Racz, M. Telek (Technical University of Budapest, Hungary)
Performability analysis of Markov reward models with rate and
impulse reward
- H. Hermanns (University of Twente, The Netherlands)
J. Kayser, M. Siegle (University of Erlangen-Nurnberg, Germany)
Multi terminal binary decision diagrams to represent and analyse
continuous time Markov chains
|
| 12h30: |
--
|
| 13h00: |
Lunch
|
| 14h30: |
MC5: Bounds (Chair: Jean-Michel Fourneau)
- S. Donatelli (Univ. de Torino, Italy)
S. Haddad (Université de Paris-Dauphine, France)
P. Moreaux, M. Sene (Université de Reims, France)
Bounds for rewards of systems with client/server interaction
- T. Dayar (Bilkent University, Ankara, Turkey)
N. Pekergin (Université de Versailles Saint Quentin, France)
Stochastic comparison, reorderings and NCD Markov chains
|
| 15h30: |
Coffee Break
|
| 16h00: |
PA2: Interactions in SPA models (Chair: Ulrich Herzog)
- J. Bradley, N. Davies (University of Bristol, UK)
Reliable performance modelling with approximate
synchronisations
- M. Bravetti, R. Gorrieri (University of Bologna, Italy)
Interactive generalized semi-Markov processes
- H. Bohnenkamp, B. Haverkort (Rheinish-Westfalishe Technische
Hochschule, Aachen, Germany)
Stochastic event structures for the decomposition of stochastic
process algebra models
|
| 17h30: |
--
|
| Friday 10 |
| 09h00: |
R. Gorrieri (Invited-PAPM/University of Bologna, Italy)
Stochastic Process algebras: past and future
|
| Track: F.1 |
| 10h00: |
PN7 (Chair: Falko Bause)
- V. Valero Ruiz, F. Cuartero Gómez (Universidad de Castilla-La
Mancha, Spain)
D. de Frutos Escrig (Univ. Complutense, Spain)
On non-decidability of reachability of timed-arc Petri nets
|
| 10h30: |
Coffee break
|
| 11h00: |
PN8: Timed Nets (Chair: Guy Juanole)
- M. Boyer, M. Diaz (LAAS/CNRS, France)
Non equivalence between Time Petri Nets and Time Stream Petri
Nets
- B. Pradin-Chezalviel, R. Valette (LAAS-CNRS, France)
L.A. Kunzle (CEFET-PR, Brasil)
Scenario durations charaterization of t-timed Petri nets using
linear logic
- X. Li, J. Lilius (Turku Centre for Computer Science, Finland)
Checking time Petri nets for linear duration properties
|
| 12h30: |
--
|
| 13h00: |
Lunch
|
| 14h30: |
MC7: Phase Type Systems (Chair: Gianfranco Ciardo)
- D. Bini, B. Meini (Univ. de Pisa, Italy)
S. Chakravarthy (Kettering University, Flint, USA)
A new algorithm for the design of finite capacity service units
- U. Krieger (Deutsche Telekom, Darmstadt, Germany)
V. Naumov (Lappeenranta University of Technology, Finland)
Analysis of a delay-loss system with a superimposed Markovian
arrival process and state-dependent service times
|
| 15h30: |
Closing Session
|
| 16h00: |
--
|
| Track: F.2 |
| 10h00: |
PA3: Probabilistic I/O Automata (Chair: Roberto Gorrieri)
- E.W. Stark, G. Pemmansani (State University of New York, Stony
Brook, USA)
Implementation of a compositional performance analysis algorithm
for probabilistic I/O automata
|
| 10h30: |
Coffee break
|
| 11h00: |
MC6: Applications (Chair: Udo Krieger)
- A. Demir, P. Feldmann (Bell laboratories, Murray Hill, USA)
Modelling and simulation of interference noise in electronic
integrated circuits using Markov chain models
- M-A. Remiche (Université Libre de Bruxelles, Belgium)
Efficiency of an IPhP^3 illustrated through a model in cellular
networks
- John Lui, W. Lam (The Chinese University of Hong Kong, Shatin, NT)
A general methodology in analyzing the performance
ofparallel/distributed simulation under general computational graphs
|
| 12h30: |
--
|
| 13h00: |
Lunch
|
| 14h30: |
PA4: SPA Case Studies (Chair: Marina Ribaudo)
- L. Kloul, J.M. Fourneau, F. Valois (Université de
Versailles-Saint Quentin, France)
Performance modelling of hierarchical cellular networks using
PEPA
- A. Aldini, M. Bernardo, R. Gorrieri (University of Bologna, Italy)
An algebraic model for evaluating the performance of an ATM switch
with explicit rate marking
|
| 15h30: |
Closing Session
|
| 16h00: |
--
|
