More Web Proxy on the site http://driver.im/

article

Bialgebraic methods and modal logic in structural operational semantics

Author:

Bartek KlinAuthors Info & Claims

Information and Computation, Volume 207, Issue 2

Pages 237 - 257

https://doi.org/10.1016/j.ic.2007.10.006

Published: 01 February 2009 Publication History

Abstract

Bialgebraic semantics, invented a decade ago by Turi and Plotkin, is an approach to formal reasoning about well-behaved structural operational semantics (SOS). An extension of algebraic and coalgebraic methods, it abstracts from concrete notions of syntax and system behaviour, thus treating various kinds of operational descriptions in a uniform fashion. In this paper, bialgebraic semantics is combined with a coalgebraic approach to modal logic in a novel, general approach to proving the compositionality of process equivalences for languages defined by structural operational semantics. To prove compositionality, one provides a notion of behaviour for logical formulas, and defines an SOS-like specification of modal operators which reflects the original SOS specification of the language. This approach can be used to define SOS congruence formats as well as to prove compositionality for specific languages and equivalences.

References

[1]

Aceto, L., Fokkink, W.J. and Verhoef, C., Structural operational semantics. In: Bergstra, J.A., Ponse, A., Smolka, S. (Eds.), Handbook of Process Algebra, Elsevier. pp. 197-292.

[2]

Aczel, P. and Mendler, N., A final coalgebra theorem. In: Proc. CTCS'89, vol. 389 of LNCS, Springer.

Digital Library

[3]

Adámek, J., Herrlich, H. and Strecker, G.E., Abstract and Concrete Categories. 1990. Wiley-Interscience.

Digital Library

[4]

Andersen, H.R., Stirling, C. and Winskel, G., A compositional proof system for the modal μ-calculus. In: Proc. LICS'94, IEEE Computer Society Press.

[5]

Baeten, J.C.M. and Middelburg, C.A., Process algebra with timing: real time and discrete time. In: Bergstra, J.A., Ponse, A., Smolka, S. (Eds.), Handbook of Process Algebra, Elsevier. pp. 627-684.

[6]

Bartels, F., GSOS for probabilistic transition systems. In: Proc. CMCS'02, vol. 65 of ENTCS, Elsevier.

[7]

F. Bartels, On generalised coinduction and probabilistic specification formats, Ph.D. dissertation, CWI, Amsterdam, 2004.

[8]

Bergstra, J.A., Ponse, A. and Smolka, S., Handbook of Process Algebra. 2002. Elsevier.

Digital Library

[9]

Bloom, B., Fokkink, W.J. and van Glabbeek, R.J., Precongruence formats for decorated trace semantics. ACM Transactions on Computational Logic. v5. 26-78.

Digital Library

[10]

Bloom, B., Istrail, S. and Meyer, A., Bisimulation can't be traced. Journal of the ACM. v42. 232-268.

Digital Library

[11]

M. Bonsangue, A. Kurz, Duality for logics of transition systems, in: Proc. FOSSACS'05, vol. 3441 of LNCS, 2005.

Digital Library

[12]

M. Bonsangue, A. Kurz, Presenting functors by operations and equations, in: Proc. FOSSACS'06, vol. 3921 of LNCS, 2006.

Digital Library

[13]

M.G. Buscemi, U. Montanari, A first order coalgebraic model of pi-calculus early observational equivalence, in: Procs. CONCUR, 2002.

Digital Library

[14]

Caires, L. and Cardelli, L., A spatial logic for concurrency (part I). Information and Computation. v186. 194-235.

Digital Library

[15]

Corradini, A., Heckel, R. and Montanari, U., Compositional SOS and beyond: a coalgebraic view of open systems. Theoretical Computer Science. v280. 163-192.

Digital Library

[16]

Fiore, M. and Staton, S., A congruence rule format for name-passing process calculi from mathematical structural operational semantics. In: Proc. LICS'06, IEEE Computer Society Press.

Digital Library

[17]

Fiore, M.P., Plotkin, G.D. and Turi, D., Abstract syntax with variable binding. In: Proc. LICS'99, IEEE Computer Society Press. pp. 193-202.

Digital Library

[18]

Fiore, M.P. and Turi, D., Semantics of name and value passing. In: Proc. LICS'01, IEEE Computer Society Press. pp. 93-104.

Digital Library

[19]

Fokkink, W. and van Glabbeek, R.J., Ntyft/ntyxt rules reduce to ntree rules. Information and Computation. v126. 1-10.

Digital Library

[20]

Fokkink, W.J., van Glabbeek, R.J. and de Wind, P., Compositionality of Hennessy--Milner logic through structural operational semantics. In: Proc. FCT'03, vol. 2751 of LNCS, Springer.

[21]

Gabbay, M.J. and Pitts, A.M., A new approach to abstract syntax with variable binding. Formal Aspects of Computing. v13. 341-363.

[22]

Glabbeek, R.J. v., The linear time---branching time spectrum I. In: Bergstra, J.A., Ponse, A., Smolka, S. (Eds.), Handbook of Process Algebra, Elsevier. pp. 3-99.

[23]

Groote, J.F., Mousavi, M. and Reniers, M.A., A hierarchy of SOS rule formats. In: Proc. SOS'05, 2005, Elsevier.

[24]

Hennessy, M. and Milner, R., Algebraic laws for nondeterminism and concurrency. Journal of the ACM. v32. 137-161.

Digital Library

[25]

B. Jacobs, Introduction to coalgebra: towards mathematics of states and observations. Available from <http://www.cs.ru.nl/B.Jacobs/CLG/JacobsCoalgebraIntro.pdf>.

[26]

Jacobs, B., Distributive laws for the coinductive solution of recursive equations. Information and Computation. v204. 561-587.

Digital Library

[27]

B. Jacobs, J.J.M.M. Rutten, A tutorial on (co)algebras and (co)induction, Bulletin of the EATCS 62.

[28]

Jonsson, B., Yi, W. and Larsen, K.G., Probabilistic extensions of process algebras. In: Bergstra, J.A., Ponse, A., Smolka, S. (Eds.), Handbook of Process Algebra, Elsevier. pp. 685-710.

[29]

Kick, M., Bialgebraic modelling of timed processes. In: Proc. ICALP'02, vol. 2380 of LNCS, Springer.

Digital Library

[30]

Kick, M., Rule formats for timed processes. In: Proc. CMCIM'02, vol. 68 of ENTCS, Elsevier.

[31]

Kick, M. and Power, J., Modularity of behaviours for mathematical operational semantics. In: Procs. CMCS'04, vol. 106 of ENTCS, Elsevier.

Digital Library

[32]

Kick, M., Power, J. and Simpson, A., Coalgebraic semantics for timed processes. Information and Computation. v204. 588-609.

Digital Library

[33]

B. Klin, Abstract coalgebraic approach to process equivalence for well-behaved operational semantics, Ph.D. thesis, BRICS, Aarhus University, 2004.

[34]

Klin, B., Adding recursive constructs to bialgebraic semantics. Journal of Logic and Algebraic Programming. v60--61. 259-286.

[35]

Klin, B., From bialgebraic semantics to congruence formats. In: Proc. SOS 2004, vol. 128 of ENTCS, Elsevier.

[36]

Klin, B., Bialgebraic metods in structural operational semantics. In: Proc. SOS'06, vol. 175 of ENTCS, Elsevier.

Digital Library

[37]

Klin, B., Bialgebraic semantics and modal logic. In: Proc. LiCS'07, IEEE Computer Society Press.

Digital Library

[38]

B. Klin, Coalgebraic modal logic beyond sets, in: Proc. MFPS 2007, vol. 173 of ENTCS, 2007.

Digital Library

[39]

Klin, B. and Sobocinski, P., Syntactic formats for free: an abstract approach to process equivalence. In: Proc. CONCUR 2003, vol. 2761 of LNCS, Springer.

[40]

A. Kurz, Logics for coalgebras and applications to computer science, Ph.D. thesis, Universität München, 2000.

[41]

A. Kurz, Coalgebras and their logics, ACM SIGACT News 37.

Digital Library

[42]

Lenisa, M., Power, J. and Watanabe, H., Distributivity for endofunctors, pointed and co-pointed endofunctors, monads and comonads. In: Proc. CMCS'00, vol. 33 of ENTCS, Elsevier. pp. 230-260.

[43]

Lenisa, M., Power, J. and Watanabe, H., Category theory for operational semantics. Theoretical Computer Science. v327 i1--2. 135-154.

Digital Library

[44]

Mac Lane, S., Categories for the Working Mathematician. 1998. second ed. Springer.

[45]

Milner, R., Communication and Concurrency. 1988. Prentice Hall.

Digital Library

[46]

Milner, R., Communicating and Mobile Systems: The π-Calculus. 1999. Cambridge University Press.

Digital Library

[47]

Monteiro, L., A noninterleaving model of concurrency based on transition systems with spatial structure. ENTCS. v106. 261-277.

Digital Library

[48]

Moss, L., Coalgebraic logic. Annals of Pure and Applied Logic. v96. 177-317.

[49]

D. Pattinson, Expressivity results in the modal logic of coalgebras, Ph.D. thesis, Universität München, 2001.

[50]

Pavlovic, D., Mislove, M. and Worrell, J.B., Testing semantics: connecting processes and process logics. In: Proc. AMAST'05, vol. 4019 of LNCS, Springer.

Digital Library

[51]

G.D. Plotkin, A structural approach to operational semantics, DAIMI Report FN-19, Computer Science Department, Aarhus University, 1981.

[52]

Power, J. and Watanabe, H., Distributivity for a monad and a comonad. In: Procs. CMCS'99, vol. 19 of ENTCS, Elsevier.

[53]

Rutten, J.J.M.M., Universal coalgebra: a theory of systems. Theoretical Computer Science. v249. 3-80.

Digital Library

[54]

L. Schröder, Expressivity of coalgebraic modal logic: the limits and beyond, in: Proc. FOSSACS'05, vol. 3441 of LNCS, 2005.

Digital Library

[55]

Simone, R.d., Higher-level synchronising devices in Meije-SCCS. Theoretical Computer Science. v37. 245-267.

[56]

Simpson, A., Sequent calculi for process verification: Hennessy--Milner logic for an arbitrary GSOS. Journal of Logic and Algebraic Programming. v60--61. 287-322.

[57]

Turi, D. and Plotkin, G.D., Towards a mathematical operational semantics. In: Proc. LICS'97, IEEE Computer Society Press. pp. 280-291.

Digital Library

Cited By

Klin B(2019)Bialgebras for structural operational semanticsTheoretical Computer Science10.1016/j.tcs.2011.03.023412:38(5043-5069)Online publication date: 6-Jan-2019
https://dl.acm.org/doi/10.1016/j.tcs.2011.03.023
Kupke C(2018)Coalgebraic Logics & DualityCoalgebraic Methods in Computer Science10.1007/978-3-030-00389-0_2(6-12)Online publication date: 14-Apr-2018
https://dl.acm.org/doi/10.1007/978-3-030-00389-0_2
Hasuo I(2017)Metamathematics for Systems DesignNew Generation Computing10.1007/s00354-017-0023-135:3(271-305)Online publication date: 1-Jul-2017
https://dl.acm.org/doi/10.1007/s00354-017-0023-1
Show More Cited By

Index Terms

Bialgebraic methods and modal logic in structural operational semantics
1. Theory of computation
  1. Logic
    1. Modal and temporal logics

Recommendations

Bialgebraic Methods in Structural Operational Semantics

Bialgebraic semantics, invented a decade ago by Turi and Plotkin, is an approach to formal reasoning about well-behaved structural operational specifications. An extension of algebraic and coalgebraic methods, it abstracts from concrete notions of ...
Structural Operational Semantics and Modal Logic, Revisited

A previously introduced combination of the bialgebraic approach to structural operational semantics with coalgebraic modal logic is re-examined and improved in some aspects. Firstly, a more abstract, conceptual proof of the main compositionality theorem ...
Coalgebraic semantics of modal logics

Coalgebras can be seen as a natural abstraction of Kripke frames. In the same sense, coalgebraic logics are generalised modal logics. In this paper, we give an overview of the basic tools, techniques and results that connect coalgebras and modal logic. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Information and Computation

Information and Computation Volume 207, Issue 2

February, 2009

288 pages

ISSN:0890-5401

Issue’s Table of Contents

Copyright © Elsevier Inc. © 2008.

Publisher

Academic Press, Inc.

United States

Publication History

Published: 01 February 2009

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

11
Total Citations
View Citations
1
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 11 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Klin B(2019)Bialgebras for structural operational semanticsTheoretical Computer Science10.1016/j.tcs.2011.03.023412:38(5043-5069)Online publication date: 6-Jan-2019
https://dl.acm.org/doi/10.1016/j.tcs.2011.03.023
Kupke C(2018)Coalgebraic Logics & DualityCoalgebraic Methods in Computer Science10.1007/978-3-030-00389-0_2(6-12)Online publication date: 14-Apr-2018
https://dl.acm.org/doi/10.1007/978-3-030-00389-0_2
Hasuo I(2017)Metamathematics for Systems DesignNew Generation Computing10.1007/s00354-017-0023-135:3(271-305)Online publication date: 1-Jul-2017
https://dl.acm.org/doi/10.1007/s00354-017-0023-1
Miculan MPeressotti M(2016)Structural operational semantics for non-deterministic processes with quantitative aspectsTheoretical Computer Science10.1016/j.tcs.2016.01.012655:PB(135-154)Online publication date: 6-Dec-2016
https://dl.acm.org/doi/10.1016/j.tcs.2016.01.012
Hoshino NMuroya KHasuo IHenzinger TMiller D(2014)Memoryful geometry of interactionProceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1145/2603088.2603124(1-10)Online publication date: 14-Jul-2014
https://dl.acm.org/doi/10.1145/2603088.2603124
Hasuo I(2011)The microcosm principle and compositionality of GSOS-based component calculiProceedings of the 4th international conference on Algebra and coalgebra in computer science10.5555/2040096.2040114(222-236)Online publication date: 30-Aug-2011
https://dl.acm.org/doi/10.5555/2040096.2040114
Hasuo IJacobs B(2011)Traces for coalgebraic componentsMathematical Structures in Computer Science10.1017/S096012951000055121:2(267-320)Online publication date: 1-Apr-2011
https://dl.acm.org/doi/10.1017/S0960129510000551
Hansen HKlin B(2011)Pointwise extensions of gsos-defined operationsMathematical Structures in Computer Science10.1017/S096012951000054X21:2(321-361)Online publication date: 1-Apr-2011
https://dl.acm.org/doi/10.1017/S096012951000054X
Hasuo I(2010)Generic forward and backward simulations IIProceedings of the 21st international conference on Concurrency theory10.5555/1887654.1887685(447-461)Online publication date: 31-Aug-2010
https://dl.acm.org/doi/10.5555/1887654.1887685
Maldonado AMonteiro LRoggenbach M(2010)Towards bialgebraic semantics for the linear time --- branching time spectrumProceedings of the 20th international conference on Recent Trends in Algebraic Development Techniques10.1007/978-3-642-28412-0_14(209-225)Online publication date: 1-Jul-2010
https://dl.acm.org/doi/10.1007/978-3-642-28412-0_14
Show More Cited By

View Options

View options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents