Keynote Presentations
Quantitative Evaluation of Service Dependability in Shared Execution Environments
Multi-agent Networked Systems with Adversarial Elements
Kronecker and Product Form Methods
A Structured Solution Approach for Markov Regenerative Processes
Low-Rank Tensor Methods for Communicating Markov Processes
Hybrid Systems
A Statistical Approach for Computing Reachability of Non-linear and Stochastic Dynamical Systems
Formal Synthesis and Validation of Inhomogeneous Thermostatically Controlled Loads
Finite Abstractions of Stochastic Max-Plus-Linear Systems
Mean Field/Population Analysis
Mean Field for Performance Models with Generally-Distributed Timed Transitions
Mean-Field Approximation and Quasi-Equilibrium Reduction of Markov Population Models
On Performance of Gossip Communication in a Crowd-Sensing Scenario
Models and Tools
Probabilistic Model Checking of DTMC Models of User Activity Patterns
Performance Comparison of IEEE 802.11 DCF and EDCA for Beaconing in Vehicular Networks
A New Great SPN GUI for GSPN Editing and CSLTA Model Checking
The Octave Queueing
Package
Simulation
A Perfect Sampling Algorithm of Random Walks with Forbidden Arcs
Modelling Replication in No SQL Datastores
Queueing, Debugging and Tools
On Queues with General Service Demands and Constant Service Capacity
Simulation Debugging and Visualization in the Mobius Modeling Framework
Scalar: A Distributed Scalability Analysis Framework
Non-intrusive Scalable Memory Access Tracer
Process Algebra and Equivalences
Probabilistic Programming Process Algebra
PALOMA: A Process Algebra for Located Markovian Agents
On the Discriminating Power of Testing Equivalences for Reactive Probabilistic Systems: Results and Open Problems
Automata and Markov Process Theory
Continuity Properties of Distances for Markov Processes
Deciding the Value 1 Problem for Reachability in 1-Clock Decision Stochastic Timed Automata
Decidable Problems for Unary PFAs
Applications, Theory and Tools
A Scalable Approach to the Assessment of Storm Impact in Distributed Automation Power Grids
Compositionality Results for Quantitative Information Flow
CyberSAGE: A Tool for Automatic Security Assessment of Cyber-Physical Systems
Probabilistic Model Checking
Symbolic Approximation of the Bounded Reachability Probability in Large Markov Chains
Accelerating Parametric Probabilistic Verification.