Abstract
Adding probabilities to timed automata enables one to carry random simulation of their behaviors and provide answers with statistical guarantees to problems otherwise untractable. Thus, when just a timed language is given, the following natural question arises: What probability should we consider if we have no a priori knowledge except the given language and the considered length (i.e. number of events) of timed words? The maximal entropy principle tells us to take the probability measure that maximises the entropy which is the uniform measure on the language restricted to timed word of the given length (with such a uniform measure every timed word has the same chance of being sampled). The uniform sampling method developed in the last decade provides no control on the duration of sampled timed words.
In the present article we consider the problem of finding a probability measure on a timed language maximising the entropy under general linear constraints on duration and for timed words of a given length. The solution we provide generalizes to timed languages a well-known result on probability measure over the real line maximising the Shannon continuous entropy under linear constraints. After giving our general theorem for general linear constraints and for general timed languages, we concentrate to the case when only the mean duration is prescribed (and again when the length is fixed) for timed languages recognised by deterministic timed automata. For this latter case, we provide an efficient sampling algorithm we have implemented and illustrated on several examples.
This work was financed by the ANR MAVeriQ (ANR-20-CE25-0012).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
In this definition the usual convention that \(0\log _2 0=1\) applies.
- 2.
One could also sample the delay before the action, this would lead at the end to the same probability distribution on timed words.
- 3.
The timed words of duration T have their timed vector \((t_1,\ldots ,t_n)\) belonging to the hyperplane \(t_1+\ldots +t_n=T\) which have a null volume. That is why we do not integrate over the last delay which is fixed and equal to \(T-t_1-\cdots -t_{n-1}\).
- 4.
Here \(\tilde{p}\) generalises the previous concept it was used for: when p depends only on duration then \(p=\tilde{p} \circ \theta \).
References
Asarin, E., Basset, N., Degorre, A.: Entropy of regular timed languages. Inf. Comput. 241, 142–176 (2015)
Barbot, B., Basset, N., Beunardeau, M., Kwiatkowska, M.: Uniform sampling for timed automata with application to language inclusion measurement. In: Agha, G., Van Houdt, B. (eds.) QEST 2016. LNCS, vol. 9826, pp. 175–190. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-43425-4_13
Barbot, B., Basset, N., Dang, T.: Generation of signals under temporal constraints for CPS testing. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2019. LNCS, vol. 11460, pp. 54–70. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-20652-9_4
Barbot, B., Basset, N., Dang, T., Donzé, A., Kapinski, J., Yamaguchi, T.: Falsification of cyber-physical systems with constrained signal spaces. In: Lee, R., Jha, S., Mavridou, A., Giannakopoulou, D. (eds.) NFM 2020. LNCS, vol. 12229, pp. 420–439. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-55754-6_25
Barbot, B., Basset, N., Donze, A.: Wordgen: a timed word generation tool. In: Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2023. Association for Computing Machinery, New York, NY, USA (2023). https://doi.org/10.1145/3575870.3587116
Basset, N.: A maximal entropy stochastic process for a timed automaton. Inf. Comput. 243, 50–74 (2015). https://doi.org/10.1016/j.ic.2014.12.006
Basset, N.: Counting and generating permutations in regular classes. Algorithmica 76(4), 989–1034 (2016). https://doi.org/10.1007/s00453-016-0136-9
Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30080-9_7
Bertrand, N., et al.: Stochastic timed automata. Log. Methods Comput. Sci. 10(4) (2014). https://doi.org/10.2168/LMCS-10(4:6)2014
Bohlender, D., Bruintjes, H., Junges, S., Katelaan, J., Nguyen, V.Y., Noll, T.: A review of statistical model checking pitfalls on real-time stochastic models. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014. LNCS, vol. 8803, pp. 177–192. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-45231-8_13
Budde, C.E., D’Argenio, P.R., Hartmanns, A., Sedwards, S.: A statistical model checker for nondeterminism and rare events. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 340–358. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89963-3_20
Cover, T.M., Thomas, J.A.: Information theory and statistics. Elem. Inf. Theory 1(1), 279–335 (1991)
Duchon, P., Flajolet, P., Louchard, G., Schaeffer, G.: Boltzmann samplers for the random generation of combinatorial structures. Comb. Probab. Comput. 13(4), 577–625 (2004). https://doi.org/10.1017/S0963548304006315
Jaynes, E.T.: Information theory and statistical mechanics. II. Phys. Rev. Online Arch. (PROLA) 108(2), 171–190 (1957)
Norman, G., Parker, D., Sproston, J.: Model checking for probabilistic timed automata. Formal Methods Syst. Des. 43(2), 164–190 (2013)
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Barbot, B., Basset, N. (2023). Max-Entropy Sampling for Deterministic Timed Automata Under Linear Duration Constraints. In: Jansen, N., Tribastone, M. (eds) Quantitative Evaluation of Systems. QEST 2023. Lecture Notes in Computer Science, vol 14287. Springer, Cham. https://doi.org/10.1007/978-3-031-43835-6_14
Download citation
DOI: https://doi.org/10.1007/978-3-031-43835-6_14
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-43834-9
Online ISBN: 978-3-031-43835-6
eBook Packages: Computer ScienceComputer Science (R0)