nach oben

Erschienen in:

2015 | OriginalPaper | Buchkapitel

On the Expressive Power of Communication Primitives in Parameterised Systems

verfasst von : Benjamin Aminof, Sasha Rubin, Florian Zuleger

Erschienen in: Logic for Programming, Artificial Intelligence, and Reasoning

Verlag: Springer Berlin Heidelberg

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

We study foundational problems regarding the expressive power of parameterised systems. These (infinite-state) systems are composed of arbitrarily many finite-state processes that synchronise using a given communication primitive, i.e., broadcast, asynchronous rendezvous, broadcast with message loss, pairwise rendezvous, or disjunctive guards. With each communication primitive we associate the class of parameterised systems that use it. We study the relative expressive power of these classes (can systems in one class be simulated by systems in another?) and provide a complete picture with only a single question left open. Motivated by the question of separating these classes, we also study the absolute expressive power (e.g., is the set of traces of every parameterised system of a given class \(\omega \)-regular?). Our work gives insight into the verification and synthesis of parameterised systems, including new decidability and undecidability results for model checking parameterised systems using broadcast with message loss and asynchronous rendezvous.

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

Vorheriges Kapitel On Subexponentials, Synthetic Connectives, and Multi-level Delimited Control

Nächstes Kapitel There Is No Best -Normalization Strategy for Higher-Order Reasoners

A cutoff is a maximal number of processes that needs to be model checked in order to guarantee correct behaviour of any number of processes. Our results show that, indeed, having a cutoff lowers the expressive power.

Typically, each label is a set of atomic propositions.

For lack of space, some proofs are missing or only sketched and can be found in the full version of this paper.

We note that the transitivity of the relations \(\le \) gives rise to additional simulations that, for clarity, are not drawn in the figures.

As in [9, 12] we formalise safety properties as regular sets (of finite words) and liveness properties as \(\omega \)-regular sets (of infinite words).

In applications one typically takes \(\varOmega := 2^{\textsf {AP}}\) where \(\textsf {AP}\) is a set of atomic predicates.

It is common to allow specifications (e.g., the LTL formula G \(_ p\)) to be satisfied by computations that loop forever in the same state. Thus, we don’t consider every transition in which the observables don’t change to be invisible. In particular, we can have both visible and invisible self loops. Using the CPU analogy, the former corresponds to a NOP in the instruction set, and the latter to a NOP in microcode.

A slightly different version of \(\textsc {bc}\), in which R is also allowed to be empty, also appears in the literature [12]. Our results also hold for this version.

If \(\textsc {cp}= \textsc {dg}\) then we also assume \(\varSigma = S\) (i.e., the synchronization alphabet is the set of local states), and for every local state \(s \in S\) there is a transition \(s \mathop {\longrightarrow }\limits ^{{t!,a}} r\) if and only if \(s = r = t\) and \(a = \mathbf {false}\) (i.e., the only transition \(\tau \) with \(\mathsf{{act}}(\tau ) = s!\) is an invisible self-loop on state s).

Although distributed systems are routinely studied this way, one may also introduce final states to the local process and restrict to runs that end in final states [16].

Abdulla, P.A., Delzanno, G., Begin, L.V.: A classification of the expressive power of well-structured transition systems. Inf. Comput. 209(3), 248–279 (2011)MATHCrossRef

Aminof, B., Kotek, T., Rubin, S., Spegni, F., Veith, H.: Parameterized model checking of rendezvous systems. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 109–124. Springer, Heidelberg (2014)

Aminof, B., Rubin, S., Zuleger, F., Spegni, F.: Liveness of parameterized timed networks. In: Halldórsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015. LNCS, vol. 9135, pp. 375–387. Springer, Heidelberg (2015) CrossRef

Aspnes, J., Ruppert, E.: An introduction to population protocols. In: Garbinato, B., Miranda, H., Rodrigues, L. (eds.) Middleware for Network Eccentric and Mobile Applications, pp. 97–120. Springer, Heidelberg (2009)CrossRef

Delzanno, G., Raskin, J.-F., Van Begin, L.: Towards the automated verification of multithreaded java programs. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 173–187. Springer, Heidelberg (2002) CrossRef

Delzanno, G., Sangnier, A., Traverso, R., Zavattaro, G.: The cost of parameterized reachability in mobile ad hoc networks. CoRR abs/1202.5850 (2012)

Delzanno, G., Sangnier, A., Zavattaro, G.: Parameterized verification of ad hoc networks. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 313–327. Springer, Heidelberg (2010) CrossRef

Delzanno, G., Sangnier, A., Zavattaro, G.: Verification of ad hoc networks with node and communication failures. In: Giese, H., Rosu, G. (eds.) FORTE 2012 and FMOODS 2012. LNCS, vol. 7273, pp. 235–250. Springer, Heidelberg (2012) CrossRef

Emerson, E., Kahlon, V.: Model checking guarded protocols. In: LICS, pp. 361–370. IEEE (2003)

10.

Emerson, E., Kahlon, V.: Reducing model checking of the many to the few. In: McAllester, D. (ed.) CADE 2000. LNCS, vol. 1831, pp. 236–254. Springer, Heidelberg (2000) CrossRef

11.

Esparza, J.: Keeping a crowd safe: on the complexity of parameterized verification. In: STACS (2014)

12.

Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: LICS, p. 352. IEEE (1999)

13.

Esparza, J., Ganty, P., Majumdar, R.: Parameterized verification of asynchronous shared-memory systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 124–140. Springer, Heidelberg (2013) CrossRef

14.

Finkel, A., Geeraerts, G., Raskin, J., Begin, L.V.: On the omega-language expressive power of extended petri nets. Theor. Comput. Sci. 356(3), 374–386 (2006)MATHCrossRef

15.

Fisher, J., Henzinger, T.A.: Executable cell biology. Nat. Biotechnol. 25(11), 1239–1249 (2007)CrossRef

16.

Geeraerts, G., Raskin, J., Begin, L.V.: Well-structured languages. Acta Inf. 44(3–4), 249–288 (2007)MATHCrossRef

17.

German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM 39(3), 675–735 (1992)MATHMathSciNetCrossRef

18.

Lynch, N.: Distributed Algorithms. Morgan Kaufman, San Francisco (1996) MATH

19.

Minsky, M.L.: Computation: Finite and Infinite Machines. Prentice-Hall, Upper Saddle River (1967) MATH

20.

Prasad, K.V.S.: A calculus of broadcasting systems. Sci. Comput. Program. 25(2–3), 285–327 (1995)CrossRef

21.

Schmitz, S., Schnoebelen, P.: The power of well-structured systems. In: D’Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013. LNCS, vol. 8052, pp. 5–24. Springer, Heidelberg (2013) CrossRef

22.

Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Banff Higher Order Workshop, pp. 238–266 (1995)

Titel: On the Expressive Power of Communication Primitives in Parameterised Systems
verfasst von: Benjamin Aminof
Sasha Rubin
Florian Zuleger
Verlag: Springer Berlin Heidelberg
Buch: Logic for Programming, Artificial Intelligence, and Reasoning
Print ISBN: 978-3-662-48898-0

Electronic ISBN: 978-3-662-48899-7

Copyright-Jahr: 2015
DOI: https://doi.org/10.1007/978-3-662-48899-7_22

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