Abstract

Probabilistic model checking mainly concentrates on techniques for reasoning about the probabilities of certain path properties or expected values of certain random variables. For the quantitative system analysis, however, there is also another type of interesting performance measure, namely quantiles. A typical quantile query takes as input a lower probability bound p and a reachability property. The task is then to compute the minimal reward bound r such that with probability at least p the target set will be reached before the accumulated reward exceeds r. Quantiles are well-known from mathematical statistics, but to the best of our knowledge they have not been addressed by the model checking community so far. In this paper, we study the complexity of quantile queries for until properties in discrete-time finite-state Markov decision processes with non-negative rewards on states. We show that qualitative quantile queries can be evaluated in polynomial time and present an exponential algorithm for the evaluation of quantitative quantile queries. For the special case of Markov chains, we show that quantitative quantile queries can be evaluated in time polynomial in the size of the chain and the maximum reward. Document type: Part of book or chapter of book

Abstract

Die vorliegende Arbeit widmet sich der simulationsbasierten Verkehrsplanung anhand eines Multi-Agenten-Ansatzes. Verkehrsplanerische Maßnahmen, wie Rück- oder Neubau von Infrastruktur, Änderungen in Fahrplänen, Maut oder Geschwindigkeitsbegrenzungen, können anhand der verwendeten Simulation (MATSim, www.matsim.org) mit einer hohen Detailgenauigkeit untersucht werden. Der Fokus liegt auf dem Verkehrsteilnehmer, der sich in der Simulation mikroskopisch durch das Verkehrssystem bewegt und in einem iterativen Prozess dessen Rahmenbedingungen lernt. Die Arbeit behandelt die Themen Lichtsignalanlagensteuerung, Luftverkehr und Softwareentwicklung. Die Arbeit zeigt, wie Lichtsignalanlagen (LSA) in der Simulation abgebildet werden können. Der Verkehrsfluss wird durch ein sehr effizient zu berechnendes „Queue Model“ (Gawron, 1998b;Simon et al., 1999; Cetin, 2005) abgebildet. Anhand einer Erweiterung des „Queue Model's“ können die Effekte von LSA abgebildet werden. Ein entwickeltes Software-Modul modelliert mikroskopische LSA. Durch die Interaktion dieses Moduls mit dem Verkehrsflussmodell können Reaktionen der Nutzer auf eine Änderung der LSA-Steuerung netzwerkweit simuliert werden. Die Resultate zeigen, dass die modellierten Wahlmöglichkeiten der Reisenden, wie z.B. Abfahrtszeit- oder Routenwahl, die Evaluation von LSA-Steuerungen beeinflussen. Verschiedene Optimierungen der LSA-Steuerung werden evaluiert. Die Optimierung von grünen Wellen hat nur geringen Einfluss auf die Verkehrsmuster. Dahingegen kommt es bei einer verkehrsabhängigen Steuerung zu netzwerkweiten Änderungen der Routen. Die Arbeit zeigt weiterhin, wie der Multi-Agenten-Ansatz zur Abbildung von Luftverkehr eingesetzt werden kann. Dabei wird das Simulationsmodul für öffentlichen Nahverkehr genutzt und entsprechend angepasst. Somit werden Passagiere auf allen Teilen ihrer Reise personenscharf abgebildet. Daraufhin wird die Verkehrsmittelwahl in die Modellierung aufgenommen. Das existierende multinomiale Logit-Modell für die Verkehrsmittelwahl (Rieser et al., 2008, Rieser, 2010) wird durch eine „Path Size Logit“-Formulierung erweitert, die Überlappungen von Routen explizit berücksichtigt. Dies behebt Artefakte des Sampling-Prozesses und ermöglicht somit die Analyse von Wettbewerbsmärkten zwischen Verkehrsträgern, z.B. zwischen Hochgeschwindigkeitszügen und Flugverbindungen. Die Software-Architektur der Simulation war anfangs monolytisch aufgebaut, funktionell schwer zu erweitern und schien für weitere Forschungszwecke nicht geeignet. In der Arbeit wird das Redesign auf eine modulare, erweiterbare Architektur erläutert. Diese soll es Forschern erlauben eigene Softwarekomponenten als Erweiterung bereitzustellen. Wie am Beispiel des Moduls für LSA gezeigt wird, ist dies möglich, sofern geeignete Schnittstellen zur Verfügung gestellt werden. Das Modul ist vom eigentlichen Simulationsprozess weitgehend abgekoppelt und kann in Teilen oder komplett ersetzt werden. This thesis aims at the simulation based assessment of transport planning using a multi-agent simulation approach. Effects of transport policies like (de-)construction of infrastructure, changes in timetable, or regulations like speed limits or tolls can be analyzed with a high level of detail by the simulation under consideration (MATSim, see www.matsim.org). Travelers are represented as individual entities that make their journey through the transport system and learn iteratively the modeled constraints. The thesis covers three areas: Traffic signal control, air transport systems, and software engineering. It is shown how traffic signal control can be simulated with the multi-agent approach. Traffic flow is simulated by a computationally efficient queue model (Gawron, 1998b;Simon et al., 1999; Cetin, 2005). In this work, the queue model is extended to capture effects of traffic signals. A software component for microscopic modeling of traffic signals is developed. This component interacts with the traffic flow model and allows the simulation of network wide effects that result from a change of traffic signal control. Results indicate that the available choice dimensions of travelers, such as route choice or departure time choice, influence the evaluation of traffic signal control. The approach is applied to test different optimizations of traffic signal control. The optimization of offsets for coordination of adjacent junctions (green waves) has little impact on the network wide traffic patterns. In contrast, a traffic-actuated signal control results in network wide changes of travelers' route choice. The thesis also shows how the multi-agent approach is applied to air transport systems. The approach uses the public transport functionality of the simulation and modifies it for air transport. As a result, individual passengers are included into the modeling on all stages of their trip. Then, mode choice between air and alternative transport modes is added. The existing Multinomial Logit model for mode choice (Rieser et al., 2008, Rieser, 2010) is enriched by a Path Size Logit formulation that takes path overlap into account. This removes artefacts of the sampling process and enables the analysis of competitive markets, e.g., between high speed rail and air transport. The software architecture of the simulation was initially a monolithic piece of software, difficult to customize, and appeared not suited for further research. The thesis discusses the redesign of the software. Design goals aim at a modular, extensible architecture that permits researchers to modify or add certain components to the overall simulation under the assumption that suitable interfaces are available. As proof of concept, the module for fixed-time traffic signal control is provided as extension. The module is decoupled from the overall simulation approach and can be replaced in part, or completely.