Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Acta Informatica
Erschienen in: Acta Informatica 2-3/2015

01.04.2015 | Original Article

On constructibility and unconstructibility of LTS operators from other LTS operators

verfasst von: Antti Valmari

Erschienen in: Acta Informatica | Ausgabe 2-3/2015

Einloggen

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

search-config
loading …

Abstract

An LTS operator can be constructed from a set of LTS operators up to an equivalence if and only if there is an LTS expression that only contains operators from the set and whose result is equivalent to the result of the operator. In this publication this idea is made precise in the context where each LTS has an alphabet of its own and the operators may depend on the alphabets. Then the extent to which LTS operators are constructible is studied. Most, if not all, established LTS operators have the property that each trace of the result arises from the execution of no more than one trace of each of its argument LTSs, and similarly for infinite traces. All LTS operators that have this property and satisfy some other rather weak regularity properties can be constructed from parallel composition and hiding up to the equivalence that compares the alphabets, traces, and infinite traces of the LTSs. Furthermore, a collection of other miscellaneous constructibility and unconstructibility results is presented.
Vorheriger Artikel CCS: It’s not fair!
Nächster Artikel Moving from interface theories to assembly theories

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 "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

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
Fußnoten
1
For any binary relation symbol \(\propto \), by “\(\propto \)” we refer to the set of pairs that specifies the relation, while \(\propto \) is used in the claims that the relation holds. That is, “\(\propto \)” \(=\) \(\{ (x,y) \mid x \propto y \}\). The benefit of this convention is illustrated by comparing \(< \cup = \ =\ \le \) to “\(<\)” \(\cup \) “\(=\)” \(=\) “\(\le \)”. More generally, we use “ and ” whenever we believe that it helps to avoid confusion.
 
Literatur
1.
Aceto, L., Fokkink, W.J., Verhoef, C.: Structural operational semantics. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, Chapter 3, pp. 197–292. Elsevier, Amsterdam (2001)CrossRef
2.
Arnold, A.: Finite Transition Systems. Prentice-Hall, Englewood Cliffs (1994)MATH
3.
4.
5.
Bolognesi, T., Brinksma, E.: Introduction to the ISO Specification Language LOTOS. Comput. Netw. ISDN Syst. 14, 25–59 (1987)CrossRef
6.
Boudol, G.: Notes on algebraic calculi of processes. In: Apt, K. (ed.) Logics and Models of Concurrent Systems, NATO ASI Series F13, pp. 261–303. Springer, Berlin (1985)CrossRef
7.
8.
Gibson-Robinson, T.: Efficient simulation of CSP-like languages. In: Welch, P.H., Barnes, F.R.M., Broenink, J.F., Chalmers, K., Pedersen, J.B., Sampson, A.T. (eds.) Communicating Process Architectures 2013, pp. 185–204. Open Channel Publishing Ltd., Bicester (2013)
9.
Gorla, D.: Towards a unified approach to encodability and separation results for process calculi. Inf. Comput. 208(9), 1031–1053 (2010)CrossRefMATHMathSciNet
10.
Kaivola, R., Valmari, A.: The weakest compositional semantic equivalence preserving nexttime-less linear temporal logic. In: Cleaveland, R. (ed.) CONCUR ’92, Third International Conference on Concurrency Theory, Lecture Notes in Computer Science, vol. 630, pp. 207–221 (1992)
11.
Karsisto, K.: A new parallel composition operator for verification tools. Dr.Tech. Thesis, Tampere University of Technology Publications 420, Tampere, Finland (2003)
12.
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems, Volume I: Specification. Springer, Berlin (1992)CrossRef
13.
Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)MATH
14.
15.
16.
Valmari, A.: Failure-based equivalences are faster than many believe. In: Desel, J. (ed.) Structures in Concurrency Theory 1995, Springer-Verlag Workshops in Computing Series, pp. 326–340 (1995)
17.
18.
Valmari, A.: Stubborn set methods for process algebras. In: Peled, D.A., Pratt, V.R., Holzmann, G.J. (eds.) Partial Order Methods in Verification: DIMACS Workshop, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 29, pp. 213–231. American Mathematical Society (1997)
19.
Valmari, A.: A Chaos-free failures divergences semantics with applications to verification. In: Davies, J., Roscoe, B., Woodcock, J. (eds.) Millennial Perspectives in Computer Science, Proceedings of the 1999 Oxford-Microsoft Symposium in Honour of sir Tony Hoare, Palgrave, pp. 365–382 (2000)
20.
Valmari, A.: All linear-time congruences for familiar operators. Log. Methods Comput. Sci. 9(11), 1–34 (2013)MathSciNet
21.
Valmari, A., Tienari, M.: Compositional failure-based semantic models for basic LOTOS. Formal Aspects Comput. 7(4), 440–468 (1995)CrossRefMATH
22.
23.
van Glabbeek, R.: Musings on encodings and expressiveness. In: Luttik, B., Reniers, M.A. (eds.) Proceedings of Combined 19th International Workshop on Expressiveness in Concurrency and 9th Workshop on Structured Operational Semantics, Electronic Proceedings in Theoretical Computer Science, vol. 89, pp. 81–98 (2012)
24.
van Glabbeek, R., Weijland, W.: Branching time and abstraction in bisimulation semantics (Extended Abstract). In: Ritter, G. (ed.) Proceedings of IFIP International Conference on Information Processing ’89, pp. 613–618. North-Holland (1989)
Metadaten
Titel
On constructibility and unconstructibility of LTS operators from other LTS operators
verfasst von
Antti Valmari
Publikationsdatum
01.04.2015
Verlag
Springer Berlin Heidelberg
Erschienen in
Acta Informatica / Ausgabe 2-3/2015
Print ISSN: 0001-5903
Elektronische ISSN: 1432-0525
DOI
https://doi.org/10.1007/s00236-015-0217-2

Weitere Artikel der Ausgabe 2-3/2015

Acta Informatica 2-3/2015 Zur Ausgabe

Original Article

CCS: It’s not fair!

Original Article

Moving from interface theories to assembly theories

Editorial

Special issue on “Comprehending asynchrony in specification and analysis” dedicated to Walter Vogler on the occasion of his 60th birthday

Original Article

Modal algebra and Petri nets

Original Article

Observable liveness of Petri nets

Original Article

Refinement checking on parametric modal transition systems