Trimming the Hedges: An Algebra to Tame Concurrency
October 2021
Pages 317 - 346
References
[1]
A. Armstrong. 2015. Formal Analysis of Concurrent Programs. Ph.D. thesis. University of Sheffield, Sheffield, UK.
[2]
A. Armstrong, V. B. F. Gomes, and G. Struth. 2014a. Algebras for program correctness in Isabelle/HOL. In RAMiCS 2014, Vol. 8428 of LNCS. Springer, 49–64.
[3]
A. Armstrong, G. Struth, and T. Weber. 2014b. Programming and automating mathematics in the Tarski–Kleene hierarchy. J. Log. Algebr. Methods Program. 83, 2, 87–102.
[4]
A. Armstrong, V. B. F. Gomes, and G. Struth. 2016. Building program construction and verification tools from algebraic principles. Form. Asp. Comput. 28, 2, 265–293.
[5]
S. L. Bloom and Z. Ésik. 1996. Free shuffle algebras in language varieties. Theor. Comput. Sci. 163, 1&2, 55–98.
[6]
P. Brunet, D. Pous, and G. Struth. 2017. On decidability of concurrent Kleene algebra. In CONCUR 2017, Vol. 85 of LIPIcs, Schloss Dagstuhl–Leibniz-Zentrum für Informatik, 28:1–28:15.
[7]
C. Calcagno, P. W. O’Hearn, and H. Yang. 2007. Local action and abstract separation logic. In Proceeding of the 22nd IEEE Conference on Logic in Computer Science. IEEE Computer Society, 366–378.
[8]
C. Calk, E. Goubault, P. Malbos, and G. Struth. 2020. Algebraic coherent confluence and higher-dimensional globular Kleene algebras. CoRR, abs/2006.16129.
[9]
E. Cohen. 2000. Separation and reduction. In MPC 2000, Vol. 1837 of LNCS. Springer, 45–59.
[10]
J. H. Conway. 1971. Regular Algebra and Finite Machines. Chapman and Hall, London, UK.
[11]
J. Cranch, S. Doherty, and G. Struth. 2020. Convolution and concurrency. CoRR, abs/2002.02321.
[12]
H.-H. Dang and B. Möller. 2012. Reverse exchange for concurrency and local reasoning. In MPC 2012, Vol. 7342 of LNCS. Springer, 177–197.
[13]
H.-H. Dang, P. Höfner, and B. Möller. 2011. Algebraic separation logic. J. Log. Algebr. Methods Program. 80, 6, 221–247.
[14]
J. Desharnais and G. Struth. 2011. Internal axioms for domain semirings. Sci. Comput. Program. 76, 3, 181–203.
[15]
J. Desharnais, B. Möller, and G. Struth. 2006. Kleene algebra with domain. ACM Trans. Comput. Log. 7, 4, 798–833.
[16]
J. Desharnais, B. Möller, and G. Struth. 2011. Algebraic notions of termination. Log. Methods Comput. Sci. 7, 1.
[17]
B. Eckmann and P. J. Hilton. 1962. Group-like structures in general categories: I. Multiplications and comultiplications. Math. Ann. 145, 227–255.
[18]
U. Fahrenberg, C. Johansen, G. Struth, and R. Bahadur Thapa. 2020. Generating posets beyond N. In RAMiCS 2020, Vol. 12062 of LNCS. Springer, 82–99.
[19]
L. Fajstrup, E. Goubault, E. Haucourt, S. Mimram, and M. Raussen. 2016. Directed Algebraic Topology and Concurrency. Springer, Switzerland.
[20]
M. P. Fiore and M. Devesas Campos. 2013. The algebra of directed acyclic graphs. In Computation, Logic, Games, and Quantum Foundations, Vol. 7860 of LNCS. Springer, 37–51.
[21]
J. L. Gischer. 1988. The equational theory of pomsets. Theor. Comput. Sci. 61, 2–3, 199–224.
[22]
V. B. F. Gomes and G. Struth. 2016. Modal Kleene algebra applied to program correctness. In FM 2016, Vol. 9995 of LNCS. 310–325.
[23]
J. Grabowski. 1981. On partial languages. Fundam. Inform. 4, 427–498.
[24]
I. J. Hayes. 2016. Generalised rely–guarantee concurrency: An algebraic foundation. Form. Asp. Comput. 28, 6, 1057–1078.
[25]
I. J. Hayes and L. A. Meinicke. 2018. Encoding fairness in a synchronous concurrent program algebra. In FM 2018, Vol. 10951 of LNCS. 222–239.
[26]
I. J. Hayes and L. A. Meinicke. 2019. Developing an algebra for rely/guarantee concurrency: Design decisions and challenges. In UTP 2019, Dedicated to Tony Hoare on the Occasion of His 85th Birthday, Vol. 11885 of LNCS. Springer, 176–197.
[27]
I. J. Hayes, C. B. Jones, and R. J. Colvin. 2012. Refining Rely–Guarantee Thinking. Technical Report CS-TR-1334, Newcastle University.
[28]
I. J. Hayes, L. A. Meinicke, K. Winter, and R. J. Colvin. 2019. A synchronous program algebra: A basis for reasoning about shared-memory and event-based concurrency. 31, 2, 133–163.
[29]
M. Herlihy and N. Shavit. 2008. The Art of Multiprocessor Programming. Morgan Kaufmann, Burlington, MA.
[30]
C. A. R. Hoare. 1972. Towards a theory of parallel programming. In Operating System Techniques, Academic Press, 61–71.
[31]
C. A. R. Hoare. 2004. Process algebra: A unifying approach. In Communicating Sequential Processes: The First 25 Years, Vol. 3525 of LNCS. Springer, 36–60.
[32]
C. A. R. Hoare, I. J. Hayes, J. He, C. Morgan, A. W. Roscoe, J. W. Sanders, I. H. Sørensen, J. M. Spivey, and B. Sufrin. 1987. Laws of programming. Commun. ACM 30, 8, 672–686.
[33]
C. A. R. Hoare, B. Möller, G. Struth, and I. Wehrman. 2009a. Concurrent Kleene algebra. In CONCUR 2009, Vol. 5710 of LNCS. Springer, 399–414.
[34]
C. A. R. Hoare, B. Möller, G. Struth, and I. Wehrman. 2009b. Foundations of concurrent Kleene algebra. In RelMiCS 2009, Vol. 5827 of LNCS. Springer, 166–186.
[35]
C. A. R. Hoare, A. Hussain, B. Möller, P. W. O’Hearn, R. Lerchedahl Petersen, and G. Struth. 2011a. On locality and the exchange law for concurrent processes. In CONCUR 2011, Vol. 6901 of LNCS. Springer, 250–264.
[36]
T. Hoare. 2005. Process algebra: A unifying approach. In M. Broy, J. Grünbauer, D. Harel, and T. Hoare (Eds.). Engineering Theories of Software Intensive Systems, Vol. 195 of NATO Science Series (Series II: Mathematics, Physics and Chemistry). Springer.
[37]
T. Hoare and S. van Staden. 2012. In praise of algebra. Form. Asp. Comput. 24, 4-6, 423–431.
[38]
T. Hoare and S. van Staden. 2014. The laws of programming unify process calculi. Sci. Comput. Program. 85, 102–114.
[39]
T. Hoare, B. Möller, G. Struth, and I. Wehrman. 2011b. Concurrent Kleene algebra and its foundations. J. Log. Algebr. Program. 80, 6, 266–296.
[40]
G. Hotz. 1965. Eine Algebraisierung des Syntheseproblems von Schaltkreisen: I. J. Inf. Process. Cybern. 1, 3, 185–205.
[41]
P. Jipsen and M. A. Moshier. 2016. Concurrent Kleene algebra with tests and branching automata. J. Log. Algebr. Methods Program. 85, 4, 637–652.
[42]
C. B. Jones. 1981. Development Methods for Computer Programs Including a Notion of Interference. Ph.D. thesis. Oxford University, Oxford, UK.
[43]
T. Kappé. 2020. Concurrent Kleene Algebra: Completeness and Decidability. Ph.D. thesis. University College London, London, UK.
[44]
T. Kappé, P. Brunet, A. Silva, and F. Zanasi. 2018. Concurrent Kleene algebra: Free model and completeness. In ESOP 2018, Vol. 10801 of LNCS. Springer, 856–882.
[45]
T. Kappé, P. Brunet, B. Luttik, A. Silva, and F. Zanasi. 2019a. On series-parallel pomset languages: Rationality, context-freeness and automata. J. Log. Algebr. Methods Program. 103, 130–153.
[46]
T. Kappé, P. Brunet, J. Rot, A. Silva, J. Wagemaker, and F. Zanasi. 2019b. Kleene algebra with observations. In CONCUR 2019, Vol. 140 of LIPIcs. Schloss Dagstuhl–Leibniz-Zentrum für Informatik, 41, 1–41:16.
[47]
T. Kappé, P. Brunet, A. Silva, J. Wagemaker, and F. Zanasi. 2020. Concurrent Kleene algebra with observations: From hypotheses to completeness. In FOSSACS 2020, Vol. 12077 of LNCS. Springer, 381–400.
[48]
S. C. Kleene. 1956. Representation of events in nerve nets and finite automata. In C. Shannon and J. McCarthy (Eds.). Automata Studies. Princeton University Press, 3–41.
[49]
D. Kozen. 1994. A completeness theorem for Kleene algebras and the algebra of regular events. Inform. Comput. 110, 2, 366–390.
[50]
D. Kozen. 1997. Kleene algebra with tests. ACM Trans. Comput. Log. 19, 3, 427–443.
[51]
D. Kozen. 2000. On Hoare logic and Kleene algebra with tests. ACM Trans. Comput. Log. 1, 1, 60–76.
[52]
M. R. Laurence and G. Struth. 2014. Completeness theorems for bi-Kleene algebras and series-parallel rational pomset languages. In RAMiCS 2014, Vol. 8428 of LNCS. Springer, 65–82.
[53]
M. R. Laurence and G. Struth. 2017. Completeness theorems for pomset languages and concurrent Kleene algebras. CoRR, abs/1705.05896.
[54]
K. Lodaya and P. Weil. 2000. Series-parallel languages and the bounded-width property. Theor. Comput. Sci. 237, 1-2, 347–380.
[55]
A. McIver, T. M. Rabehaja, and G. Struth. 2011. On probabilistic Kleene algebras, automata and simulations. In RAMICS 2011, Vol. 6663 of LNCS. Springer, 264–279.
[56]
A. McIver, T. M. Rabehaja, and G. Struth. 2013a. Probabilistic concurrent Kleene algebra. In QAPL 2013, 97–115.
[57]
A. McIver, T. M. Rabehaja, and G. Struth. 2013b. Weak concurrent Kleene algebra with application to algebraic verification. CoRR, abs/1301.7153.
[58]
A. McIver, T. M. Rabehaja, and G. Struth. 2013c. An event structure model for probabilistic concurrent Kleene algebra. In LPAR-19, Vol. 8312 of LNCS. Springer, 653–667.
[59]
A. McIver, T. M. Rabehaja, and G. Struth. 2016. Probabilistic rely–guarantee calculus. Theor. Comput. Sci. 655, 120–134.
[60]
J. Meseguer and U. Montanari. 1990. Petri nets are monoids. Inform. Comput. 88, 2, 105–155.
[61]
B. Möller and T. Hoare. 2015. Exploring an interface model for CKA. In MPC 2015, Vol. 9129 of LNCS. Springer, 1–29.
[62]
B. Möller, T. Hoare, M. E. Müller, and G. Struth. 2016. A discrete geometric model of concurrent program execution. In UTP 2016, Vol. 10134 of LNCS. Springer, 1–25.
[63]
P. W. O’Hearn. 2007. Resources, concurrency, and local reasoning. Theor. Comput. Sci. 375, 1–3, 271–307.
[64]
P. W. O’Hearn, R. Lerchedahl Petersen, J. Villard, and A. Hussain. 2015. On the relation between concurrent separation logic and concurrent Kleene algebra. J. Log. Algebr. Methods Program. 84, 3, 285–302.
[65]
V. R. Pratt. 1982. On the composition of processes. In Proceedings of the 9th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. ACM Press, 213–223.
[66]
C. Prisacariu. 2010. Synchronous Kleene algebra. J. Log. Algebr. Methods Program. 79, 7, 608–635.
[67]
T. M. Rabehaja. 2014. Algebraic Verification of Probabilistic and Concurrent Systems. Ph.D. thesis. Macquarie University and University of Sheffield, Sheffield, UK, and Sydney, Australia.
[68]
G. Struth. 2008. Modal tools for separation and refinement. Electron. Notes Theor. Comput. Sci. 214, 81–101.
[69]
A. Tarlecki. 1985. A language of specified programs. Sci. Comput. Program. 5, 1, 59–81.
[70]
S. van Staden and T. Hoare. 2012. Algebra unifies operational calculi. In UTP 2012, Vol. 7681 of LNCS. 88–104.
[71]
J. von Wright. 2002. From Kleene algebra to refinement algebra. In MPC 2002, Vol. 2386 of LNCS. Springer, 233–262.
[72]
J. von Wright. 2004. Towards a refinement algebra. Sci. Comput. Program. 51, 1–2, 23–45.
[73]
I. Wehrman, C. A. R. Hoare, and P. W. O’Hearn. 2009. Graphical models of separation logic. Inf. Process. Lett. 109, 17, 1001–1004.
[74]
J. Winkowski. 1977. Algebras of partial sequences—A tool to deal with concurrency. In FOCS 1977, Vol. 56 of LNCS. Springer, 187–198.
Index Terms
- Trimming the Hedges: An Algebra to Tame Concurrency
Index terms have been assigned to the content through auto-classification.
Recommendations
Multi-adjoint lattice logic and truth-stressing hedges
AbstractThis paper presents the multi-adjoint lattice logic (MLL) and its completeness and soundness. Specifically, the proposed many-valued propositional logic framework is defined on a multi-adjoint algebra whose underlying algebraic structure is a ...
Proposition algebra
Sequential propositional logic deviates from conventional propositional logic by taking into account that during the sequential evaluation of a propositional statement, atomic propositions may yield different Boolean values at repeated occurrences. We ...
On v-filters of Residuated Lattices with Hedges
FSKD '09: Proceedings of the 2009 Sixth International Conference on Fuzzy Systems and Knowledge Discovery - Volume 06In this paper, based on Hajek, Vychodil, Rachunek and Salounova's works, we introduce and study the concept ofv-filters of residuated lattices with two hedges. We give the formulas for calculating the v-filters generated by subsets, and show that the ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 02 October 2021
Check for updates
Qualifiers
- Chapter
Appears in
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 7Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 20 Nov 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in