-
On-The-Fly Symbolic Algorithm for Timed ATL with Abstractions
Authors:
Nicolaj Ø. Jensen,
Kim G. Larsen,
Didier Lime,
Jiří Srba
Abstract:
Verification of real-time systems with multiple components controlled by multiple parties is a challenging task due to its computational complexity. We present an on-the-fly algorithm for verifying timed alternating-time temporal logic (TATL), a branching-time logic with quantifiers over outcomes that results from coalitions of players in such systems. We combine existing work on games and timed C…
▽ More
Verification of real-time systems with multiple components controlled by multiple parties is a challenging task due to its computational complexity. We present an on-the-fly algorithm for verifying timed alternating-time temporal logic (TATL), a branching-time logic with quantifiers over outcomes that results from coalitions of players in such systems. We combine existing work on games and timed CTL verification in the abstract dependency graph (ADG) framework, which allows for easy creation of on-the-fly algorithms that only explore the state space as needed. In addition, we generalize the conventional inclusion check to the ADG framework which enables dynamic reductions of the dependency graph. Using the insights from the generalization, we present a novel abstraction that eliminates the need for inclusion checking altogether in our domain. We implement our algorithms in Uppaal and our experiments show that while inclusion checking considerably enhances performance, our abstraction provides even more significant improvements, almost two orders of magnitude faster than the naive method. In addition, we outperform Uppaal Tiga, which can verify only a strict subset of TATL. After implementing our new abstraction in Uppaal Tiga, we also improve its performance by almost an order of magnitude.
△ Less
Submitted 9 June, 2025;
originally announced June 2025.
-
Spectroscopic observations of flares and superflares on AU Mic
Authors:
P. Odert,
M. Leitzinger,
R. Greimel,
P. Kabáth,
J. Lipták,
P. Heinzel,
R. Karjalainen,
J. Wollmann,
E. W. Guenther,
M. Skarka,
J. Srba,
P. Škoda,
J. Frýda,
R. Brahm,
L. Vanzi,
J. Janík
Abstract:
The young active flare star AU~Mic is the planet host star with the highest flare rate from TESS data. Therefore, it represents an ideal target for dedicated ground-based monitoring campaigns with the aim to characterize its numerous flares spectroscopically. We performed such spectroscopic monitoring with the ESO1.52m telescope of the PLATOSpec consortium. In more than 190 hours of observations,…
▽ More
The young active flare star AU~Mic is the planet host star with the highest flare rate from TESS data. Therefore, it represents an ideal target for dedicated ground-based monitoring campaigns with the aim to characterize its numerous flares spectroscopically. We performed such spectroscopic monitoring with the ESO1.52m telescope of the PLATOSpec consortium. In more than 190 hours of observations, we find 24 flares suitable for detailed analysis. We compute their parameters (duration, peak flux, energy) in eight chromospheric lines (H$α$, H$β$, H$γ$, H$δ$, Na I D1&D2, He I D3, He I 6678) and investigate their relationships. Furthermore, we obtained simultaneous photometric observations and low-resolution spectroscopy for part of the spectroscopic runs. We detect one flare in the g'-band photometry which is associated with a spectroscopic flare. Additionally, an extreme flare event occurred on 2023-09-16 of which only a time around its possible peak was observed, during which chromospheric line fluxes were raised by up to a factor of three compared to the following night. The estimated energy of this event is around $10^{33}$ erg in H$α$ alone, i.e. a rare chromospheric line superflare.
△ Less
Submitted 12 December, 2024;
originally announced December 2024.
-
HD 110067 c has an aligned orbit
Authors:
J. Zak,
H. M. J. Boffin,
E. Sedaghati,
A. Bocchieri,
Q. Changeat,
A. Fukui,
A. Hatzes,
T. Hillwig,
K. Hornoch,
D. Itrich,
V. D. Ivanov,
D. Jones,
P. Kabath,
Y. Kawai,
L. V. Mugnai,
F. Murgas,
N. Narita,
E. Palle,
E. Pascale,
P. Pravec,
S. Redfield,
G. Roccetti,
M. Roth,
J. Srba,
Q. Tian
, et al. (3 additional authors not shown)
Abstract:
Planetary systems in mean motion resonances hold a special place among the planetary population. They allow us to study planet formation in great detail as dissipative processes are thought to have played an important role in their existence. Additionally, planetary masses in bright resonant systems may be independently measured both by radial velocities (RVs) and transit timing variations (TTVs).…
▽ More
Planetary systems in mean motion resonances hold a special place among the planetary population. They allow us to study planet formation in great detail as dissipative processes are thought to have played an important role in their existence. Additionally, planetary masses in bright resonant systems may be independently measured both by radial velocities (RVs) and transit timing variations (TTVs). In principle, they also allow us to quickly determine the inclination of all planets in the system, as for the system to be stable, they are likely all in coplanar orbits. To describe the full dynamical state of the system, we also need the stellar obliquity that provides the orbital alignment of a planet with respect to the spin of their host star and can be measured thanks to the Rossiter-McLaughlin effect. It was recently discovered that HD 110067 harbours a system of six sub-Neptunes in resonant chain orbits. We here analyze an ESPRESSO high-resolution spectroscopic time series of HD 110067 during the transit of planet c. We find the orbit of HD 110067 c to be well aligned with sky projected obliquity $λ=6^{+24}_{-26}$ deg. This result is indicative that the current architecture of the system has been reached through convergent migration without any major disruptive events. Finally, we report transit-timing variation in this system as we find a significant offset of 19 $\pm$ 4 minutes in the center of the transit compared to the published ephemeris.
△ Less
Submitted 28 May, 2024; v1 submitted 20 May, 2024;
originally announced May 2024.
-
Methods for Efficient Unfolding of Colored Petri Nets
Authors:
Alexander Bilgram,
Peter G. Jensen,
Thomas Pedersen,
Jiri Srba,
Peter H. Taankvist
Abstract:
Colored Petri nets offer a compact and user friendly representation of the traditional P/T nets and colored nets with finite color ranges can be unfolded into the underlying P/T nets, however, at the expense of an exponential explosion in size. We present two novel techniques based on static analysis in order to reduce the size of unfolded colored nets. The first method identifies colors that beha…
▽ More
Colored Petri nets offer a compact and user friendly representation of the traditional P/T nets and colored nets with finite color ranges can be unfolded into the underlying P/T nets, however, at the expense of an exponential explosion in size. We present two novel techniques based on static analysis in order to reduce the size of unfolded colored nets. The first method identifies colors that behave equivalently and groups them into equivalence classes, potentially reducing the number of used colors. The second method overapproximates the sets of colors that can appear in places and excludes colors that can never be present in a given place. Both methods are complementary and the combined approach allows us to significantly reduce the size of multiple colored Petri nets from the Model Checking Contest benchmark. We compare the performance of our unfolder with state-of-the-art techniques implemented in the tools MCC, Spike and ITS-Tools, and while our approach is competitive w.r.t. unfolding time, it also outperforms the existing approaches both in the size of unfolded nets as well as in the number of answered model checking queries from the 2021 Model Checking Contest.
△ Less
Submitted 11 October, 2023; v1 submitted 12 April, 2022;
originally announced April 2022.
-
Learning Safe and Optimal Control Strategies for Storm Water Detention Ponds
Authors:
Martijn A. Goorden,
Kim G. Larsen,
Jesper E. Nielsen,
Thomas D. Nielsen,
Michael R. Rasmussen,
Jiri Srba
Abstract:
Storm water detention ponds are used to manage the discharge of rainfall runoff from urban areas to nearby streams. Their purpose is to reduce the hydraulic impact and sediment loads of the receiving waters. Detention ponds are currently designed based on static controls: the output flow of a pond is capped at a fixed value. This is not optimal with respect to the current infrastructure capacity a…
▽ More
Storm water detention ponds are used to manage the discharge of rainfall runoff from urban areas to nearby streams. Their purpose is to reduce the hydraulic impact and sediment loads of the receiving waters. Detention ponds are currently designed based on static controls: the output flow of a pond is capped at a fixed value. This is not optimal with respect to the current infrastructure capacity and for some detention ponds it might even violate current regulations set by the European Water Framework Directive. We apply formal methods to synthesize (i.e., derive automatically) a safe and optimal active controller. We model the storm water detention pond, including the urban catchment area and the rain forecasts, as a hybrid Markov decision process. Subsequently, we use the tool Uppaal Stratego to synthesize a control strategy minimizing the cost related to pollution (optimality) while guaranteeing no emergency overflow of the detention pond (safety). Simulation results for an existing pond show that Uppaal Stratego can learn optimal strategies that prevent emergency overflows, where the current static control is not always able to prevent it. At the same time, our approach can improve sedimentation during low rain periods.
△ Less
Submitted 26 April, 2021;
originally announced April 2021.
-
Stubborn Set Reduction for Two-Player Reachability Games
Authors:
Frederik Meyer Bønneland,
Peter Gjøl Jensen,
Kim Guldstrand Larsen,
Marco Muñiz,
Jiří Srba
Abstract:
Partial order reductions have been successfully applied to model checking of concurrent systems and practical applications of the technique show nontrivial reduction in the size of the explored state space. We present a theory of partial order reduction based on stubborn sets in the game-theoretical setting of 2-player games with reachability objectives. Our stubborn reduction allows us to prune t…
▽ More
Partial order reductions have been successfully applied to model checking of concurrent systems and practical applications of the technique show nontrivial reduction in the size of the explored state space. We present a theory of partial order reduction based on stubborn sets in the game-theoretical setting of 2-player games with reachability objectives. Our stubborn reduction allows us to prune the interleaving behaviour of both players in the game, and we formally prove its correctness on the class of games played on general labelled transition systems. We then instantiate the framework to the class of weighted Petri net games with inhibitor arcs and provide its efficient implementation in the model checker TAPAAL. Finally, we evaluate our stubborn reduction on several case studies and demonstrate its efficiency.
△ Less
Submitted 17 March, 2021; v1 submitted 20 December, 2019;
originally announced December 2019.
-
Proceedings Cassting Workshop on Games for the Synthesis of Complex Systems and 3rd International Workshop on Synthesis of Complex Parameters
Authors:
Thomas Brihaye,
Benoît Delahaye,
Loïg Jezequel,
Nicolas Markey,
Jiří Srba
Abstract:
This volume contains the joint proceedings of the Workshop on Games for the Synthesis of Complex Systems (CASSTING'16) and of the 3rd International Workshop on Synthesis of Complex Parameters (SynCoP'16). The workshops were held in Eindhoven, The Netherlands, as satellite events of the 19th European Joint Conferences on Theory and Practice of Software (ETAPS'16). Both workshops are closely relate…
▽ More
This volume contains the joint proceedings of the Workshop on Games for the Synthesis of Complex Systems (CASSTING'16) and of the 3rd International Workshop on Synthesis of Complex Parameters (SynCoP'16). The workshops were held in Eindhoven, The Netherlands, as satellite events of the 19th European Joint Conferences on Theory and Practice of Software (ETAPS'16). Both workshops are closely related in their topics as well as target audience and they shared a joint invited talk given by Giorgio Delzanno.
△ Less
Submitted 30 July, 2016;
originally announced August 2016.
-
Language Emptiness of Continuous-Time Parametric Timed Automata
Authors:
Nikola Beneš,
Peter Bezděk,
Kim G. Larsen,
Jiří Srba
Abstract:
Parametric timed automata extend the standard timed automata with the possibility to use parameters in the clock guards. In general, if the parameters are real-valued, the problem of language emptiness of such automata is undecidable even for various restricted subclasses. We thus focus on the case where parameters are assumed to be integer-valued, while the time still remains continuous. On the o…
▽ More
Parametric timed automata extend the standard timed automata with the possibility to use parameters in the clock guards. In general, if the parameters are real-valued, the problem of language emptiness of such automata is undecidable even for various restricted subclasses. We thus focus on the case where parameters are assumed to be integer-valued, while the time still remains continuous. On the one hand, we show that the problem remains undecidable for parametric timed automata with three clocks and one parameter. On the other hand, for the case with arbitrary many clocks where only one of these clocks is compared with (an arbitrary number of) parameters, we show that the parametric language emptiness is decidable. The undecidability result tightens the bounds of a previous result which assumed six parameters, while the decidability result extends the existing approaches that deal with discrete-time semantics only. To the best of our knowledge, this is the first positive result in the case of continuous-time and unbounded integer parameters, except for the rather simple case of single-clock automata.
△ Less
Submitted 29 April, 2015;
originally announced April 2015.
-
Note on Undecidability of Bisimilarity for Second-Order Pushdown Processes
Authors:
Petr Jančar,
Jiří Srba
Abstract:
Broadbent and Göller (FSTTCS 2012) proved the undecidability of bisimulation equivalence for processes generated by epsilon-free second-order pushdown automata. We add a few remarks concerning the used proof technique, called Defender's forcing, and the related undecidability proof for first-order pushdown automata with epsilon-transitions (Jančar and Srba, JACM 2008).
Broadbent and Göller (FSTTCS 2012) proved the undecidability of bisimulation equivalence for processes generated by epsilon-free second-order pushdown automata. We add a few remarks concerning the used proof technique, called Defender's forcing, and the related undecidability proof for first-order pushdown automata with epsilon-transitions (Jančar and Srba, JACM 2008).
△ Less
Submitted 4 March, 2013;
originally announced March 2013.
-
Time-Darts: A Data Structure for Verification of Closed Timed Automata
Authors:
Kenneth Y. Jørgensen,
Kim G. Larsen,
Jiří Srba
Abstract:
Symbolic data structures for model checking timed systems have been subject to a significant research, with Difference Bound Matrices (DBMs) still being the preferred data structure in several mature verification tools. In comparison, discretization offers an easy alternative, with all operations having linear-time complexity in the number of clocks, and yet valid for a large class of closed syste…
▽ More
Symbolic data structures for model checking timed systems have been subject to a significant research, with Difference Bound Matrices (DBMs) still being the preferred data structure in several mature verification tools. In comparison, discretization offers an easy alternative, with all operations having linear-time complexity in the number of clocks, and yet valid for a large class of closed systems. Unfortunately, fine-grained discretization causes itself a state-space explosion. We introduce a new data structure called time-darts for the symbolic representation of state-spaces of timed automata. Compared with the complete discretization, a single time-dart allows to represent an arbitrary large set of states, yet the time complexity of operations on time-darts remain linear in the number of clocks. We prove the correctness of the suggested reachability algorithm and perform several experiments in order to compare the performance of time-darts and the complete discretization. The main conclusion is that in all our experiments the time-dart method outperforms the complete discretization and it scales significantly better for models with larger constants.
△ Less
Submitted 26 November, 2012;
originally announced November 2012.
-
A Forward Reachability Algorithm for Bounded Timed-Arc Petri Nets
Authors:
Alexandre David,
Lasse Jacobsen,
Morten Jacobsen,
Jiří Srba
Abstract:
Timed-arc Petri nets (TAPN) are a well-known time extension of the Petri net model and several translations to networks of timed automata have been proposed for this model. We present a direct, DBM-based algorithm for forward reachability analysis of bounded TAPNs extended with transport arcs, inhibitor arcs and age invariants. We also give a complete proof of its correctness, including reduction…
▽ More
Timed-arc Petri nets (TAPN) are a well-known time extension of the Petri net model and several translations to networks of timed automata have been proposed for this model. We present a direct, DBM-based algorithm for forward reachability analysis of bounded TAPNs extended with transport arcs, inhibitor arcs and age invariants. We also give a complete proof of its correctness, including reduction techniques based on symmetries and extrapolation. Finally, we augment the algorithm with a novel state-space reduction technique introducing a monotonic ordering on markings and prove its soundness even in the presence of monotonicity-breaking features like age invariants and inhibitor arcs. We implement the algorithm within the model-checker TAPAAL and the experimental results document an encouraging performance compared to verification approaches that translate TAPN models to UPPAAL timed automata.
△ Less
Submitted 26 November, 2012;
originally announced November 2012.
-
Beyond Language Equivalence on Visibly Pushdown Automata
Authors:
Jiří Srba
Abstract:
We study (bi)simulation-like preorder/equivalence checking on the class of visibly pushdown automata and its natural subclasses visibly BPA (Basic Process Algebra) and visibly one-counter automata. We describe generic methods for proving complexity upper and lower bounds for a number of studied preorders and equivalences like simulation, completed simulation, ready simulation, 2-nested simulatio…
▽ More
We study (bi)simulation-like preorder/equivalence checking on the class of visibly pushdown automata and its natural subclasses visibly BPA (Basic Process Algebra) and visibly one-counter automata. We describe generic methods for proving complexity upper and lower bounds for a number of studied preorders and equivalences like simulation, completed simulation, ready simulation, 2-nested simulation preorders/equivalences and bisimulation equivalence. Our main results are that all the mentioned equivalences and preorders are EXPTIME-complete on visibly pushdown automata, PSPACE-complete on visibly one-counter automata and P-complete on visibly BPA. Our PSPACE lower bound for visibly one-counter automata improves also the previously known DP-hardness results for ordinary one-counter automata and one-counter nets. Finally, we study regularity checking problems for visibly pushdown automata and show that they can be decided in polynomial time.
△ Less
Submitted 26 January, 2009; v1 submitted 14 January, 2009;
originally announced January 2009.
-
Interprocedural Dataflow Analysis over Weight Domains with Infinite Descending Chains
Authors:
Morten Kühnrich,
Stefan Schwoon,
Jiří Srba,
Stefan Kiefer
Abstract:
We study generalized fixed-point equations over idempotent semirings and provide an efficient algorithm for the detection whether a sequence of Kleene's iterations stabilizes after a finite number of steps. Previously known approaches considered only bounded semirings where there are no infinite descending chains. The main novelty of our work is that we deal with semirings without the boundednes…
▽ More
We study generalized fixed-point equations over idempotent semirings and provide an efficient algorithm for the detection whether a sequence of Kleene's iterations stabilizes after a finite number of steps. Previously known approaches considered only bounded semirings where there are no infinite descending chains. The main novelty of our work is that we deal with semirings without the boundedness restriction. Our study is motivated by several applications from interprocedural dataflow analysis. We demonstrate how the reachability problem for weighted pushdown automata can be reduced to solving equations in the framework mentioned above and we describe a few applications to demonstrate its usability.
△ Less
Submitted 6 January, 2009; v1 submitted 5 January, 2009;
originally announced January 2009.
