nach oben

Erschienen in:

2017 | OriginalPaper | Buchkapitel

An Automata-Theoretic Approach to Modeling Systems and Specifications over Infinite Data

verfasst von : Hadar Frenkel, Orna Grumberg, Sarai Sheinvald

Erschienen in: NASA Formal Methods

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Data-parameterized systems model finite state systems over an infinite data domain. VLTL is an extension of LTL that uses variables in order to specify properties of computations over infinite data, and as such VLTL is suitable for specifying properties of data-parameterized systems. We present Alternating Variable Büchi Word Automata (AVBWs), a new model of automata over infinite alphabets, capable of modeling a significant fragment of VLTL. While alternating and non-deterministic Büchi automata over finite alphabets have the same expressive power, we show that this is not the case for infinite data domains, as we prove that AVBWs are strictly stronger than the previously defined Non-deterministic Variable Büchi Word Automata (NVBWs). However, while the emptiness problem is easy for NVBWs, it is undecidable for AVBWs. We present an algorithm for translating AVBWs to NVBWs in cases where such a translation is possible. Additionally, we characterize the structure of AVBWs that can be translated to NVBWs with our algorithm, and identify fragments of VLTL for which a direct NVBW construction exists. Since the emptiness problem is crucial in the automata-theoretic approach to model checking, our results give rise to a model-checking algorithm for a rich fragment of VLTL and systems over infinite data domains.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Nächstes Kapitel Learning from Faults: Mutation Testing in Active Automata Learning

In particular, the negation operator is not included.

The semantics of \(\lnot a.x\) is regarding a specific value. I.e., if \(x=d\) then a.d does not hold, but \(a.d'\) for \(d\ne d'\) may hold.

Comments to the algorithm are given in gray.

In [17] the authors conjecture without proof that the formula \(\textsf {G}\, \exists x: a.x\) does not have an equivalent in PNF. In Lemma 1 we showed \(\textsf {G}\, \exists x(b.x\wedge \textsf {F}\, a.x)\) does not have an equivalent NVBW, thus it does not have an equivalent \(\exists ^*_{pnf}\)-VLTL formula. This is a different formula from \(\textsf {G}\, \exists x: a.x\), but the conclusion remains the same.

Barringer, H., Falcone, Y., Havelund, K., Reger, G., Rydeheard, D.: Quantified event automata: towards expressive and efficient runtime monitors. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 68–84. Springer, Heidelberg (2012). doi:10.1007/978-3-642-32759-9_9 CrossRef

Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. 20(4), 14:1–14:64 (2011)CrossRef

Bojańczyk, M., Muscholl, A., Schwentick, T., Segoufin, L., David, C.: Two-variable logic on words with data. In: 21st IEEE Symposium on Logic in Computer Science (LICS 2006), 12–15, Seattle, WA, USA, Proceedings, pp. 7–16. IEEE Computer Society, 2006, August 2006

Bouajjani, A., Habermehl, P., Jurski, Y., Sighireanu, M.: Rewriting systems with data. In: Csuhaj-Varjú, E., Ésik, Z. (eds.) FCT 2007. LNCS, vol. 4639, pp. 1–22. Springer, Heidelberg (2007). doi:10.1007/978-3-540-74240-1_1 CrossRef

Brambilla, M., Ceri, S., Comai, S., Fraternali, P., Manolescu, I.: Specification and design of workflow-driven hypertexts. J. Web Eng. 1(2), 163–182 (2003)

J. R. Buechi. On a decision method in restricted second-order arithmetic. In International Congress on Logic, Methodology, and Philosophy of Science, pp. 1–11. Stanford University Press, (1962)

Ceri, S., Matera, M., Rizzo, F., Demaldé, V.: Designing data-intensive web applications for content accessibility using web marts. Commun. ACM 50(4), 55–61 (2007)CrossRef

Colin, S., Mariani, L.: Run-time verification. In: Broy, M., Jonsson, B., Katoen, J.-P., Leucker, M., Pretschner, A. (eds.) Model-Based Testing of Reactive Systems. LNCS, vol. 3472, pp. 525–555. Springer, Heidelberg (2005). doi:10.1007/11498490_24 CrossRef

Emerson, E.A., Halpern, J.Y.: “sometimes” and “not never” revisited: on branching versus linear time temporal logic. J. ACM 33(1), 151–178 (1986)MathSciNetCrossRefMATH

10.

Grumberg, O., Kupferman, O., Sheinvald, S.: Variable Automata over Infinite Alphabets. In: Dediu, A.-H., Fernau, H., Martín-Vide, C. (eds.) LATA 2010. LNCS, vol. 6031, pp. 561–572. Springer, Heidelberg (2010). doi:10.1007/978-3-642-13089-2_47 CrossRef

11.

Grumberg, O., Kupferman, O., Sheinvald, S.: Model checking systems and specifications with parameterized atomic propositions. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, pp. 122–136. Springer, Heidelberg (2012). doi:10.1007/978-3-642-33386-6_11 CrossRef

12.

Grumberg, O., Kupferman, O., Sheinvald, S.: A game-theoretic approach to simulation of data-parameterized systems. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 348–363. Springer, Cham (2014). doi:10.1007/978-3-319-11936-6_25

13.

Kaminski, M., Francez, N.: Finite-memory automata. Theor. Comput. Sci. 134(2), 329–363 (1994)MathSciNetCrossRefMATH

14.

Miyano, S., Hayashi, T.: Alternating finite automata on omega-words. Theor. Comput. Sci. 32, 321–330 (1984)MathSciNetCrossRefMATH

15.

Muller, D., Schupp, P.E.: Alternating automata on infinite objects, determinacy and Rabin’s theorem. In: Nivat, M., Perrin, D. (eds.) LITP 1984. LNCS, vol. 192, pp. 99–107. Springer, Heidelberg (1985). doi:10.1007/3-540-15641-0_27 CrossRef

16.

Neven, F., Schwentick, T., Vianu, V.: Towards regular languages over infinite alphabets. In: Sgall, J., Pultr, A., Kolman, P. (eds.) MFCS 2001. LNCS, vol. 2136, pp. 560–572. Springer, Heidelberg (2001). doi:10.1007/3-540-44683-4_49 CrossRef

17.

Song, F., Wu, Z.: Extending temporal logics with data variable quantifications. In: Raman, V., Suresh, S.P. (eds.) 34th International Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 15–17, 2014, New Delhi, India, vol. 29 of LIPIcs, pp. 253–265. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2014, December 2014

18.

Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol. 1043, pp. 238–266. Springer, Heidelberg (1996). doi:10.1007/3-540-60915-6_6 CrossRef

19.

Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (preliminary report). In: Proceedings of the Symposium on Logic in Computer Science (LICS 1986), Cambridge, Massachusetts, USA, June 16–18, pp. 332–344. IEEE Computer Society (1986)

Titel: An Automata-Theoretic Approach to Modeling Systems and Specifications over Infinite Data
verfasst von: Hadar Frenkel
Orna Grumberg
Sarai Sheinvald
Verlag: Springer International Publishing
Buch: NASA Formal Methods
Print ISBN: 978-3-319-57287-1

Electronic ISBN: 978-3-319-57288-8

Copyright-Jahr: 2017
DOI: https://doi.org/10.1007/978-3-319-57288-8_1

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner