International audience

Abstract We propose a novel state-space reduction framework to improve the performance of model checking of Petri nets. We provide two instances of the framework: a static technique that considers only the structure of the net, and a dynamic technique that additionally considers the current marking. By analyzing impossible, visible, and directional effects of transitions, we identify places where tokens can be removed while preserving the property in question. Unlike structural reductions, our techniques modify only the current marking, allowing the net structure to be reused in multiple subproblems concurrently, which can be beneficial for example for CTL model checking. We prove the correctness of our techniques and implement them in the open-source tool Tapaal, a repeated winner in the CTL category in the annual model checking contest (MCC). We measure our methods’ performance on the MCC 2023 benchmark using the CTL categories and demonstrate that our methods reduce time and, especially, memory usage. Our dynamic method explores 39.3% fewer configurations on average and achieves two orders of magnitude speedup on at least one query on 23.7% of non-trivial models.

The SUMO traffic simulator is a mainstream tool that allows to model and analyse traffic and mobility scenarios. Fully realistic scenarios can be appealing for many use cases, but they require an initial large investment of resources for their creation. In fact, the usual workflow comprises the manual creation of a statistics file with detailed information about the city and its properties, up to describing how many people live and work on each road. This step is followed by the application of the tool ACTIVITYGEN to generate activity-based traffic. Current alternatives are based on simple randomly generated traffic, such as by means of the tool randomTrips. We present a compromise between the two approaches, consisting of mathematical techniques to generate schools, city gates, population density with residential and industrial areas, and a city centre. We also introduce an accompanying tool, randomActivityGen, which implements the approach to create ACTIVITYGEN statistics files automatically. Evaluation of generated scenarios shows that population and industry density, schools, and city-gates are placed realistically through testing on five representative Danish cities. The approach is also compared with the output of the tool randomTrips and the LuST scenario.