Hostname: page-component-586b7cd67f-dlnhk Total loading time: 0 Render date: 2024-11-28T14:57:14.041Z Has data issue: false hasContentIssue false
  • English
  • Français

Algebra and logic for resource-based systems modelling

Published online by Cambridge University Press:  04 September 2009

MATTHEW COLLINSON  and
DAVID PYM
MATTHEW COLLINSON
Affiliation:
Hewlett-Packard Laboratories, Bristol, BS34 8QZ, United Kingdom
DAVID PYM
Affiliation:
Hewlett-Packard Laboratories, Bristol, BS34 8QZ, United Kingdom University of Bath, Bath, BA2 7AY, United Kingdom
Get access Rights & Permissions [Opens in a new window]

Abstract

Mathematical modelling is one of the fundamental tools of science and engineering. Very often, models are required to be executable, as a simulation, on a computer. In this paper, we present some contributions to the process-theoretic and logical foundations of discrete-event modelling with resources and processes. We present a process calculus with an explicit representation of resources in which processes and resources co-evolve. The calculus is closely connected to a logic that may be used as a specification language for properties of models. The logic is strong enough to allow requirements that a system has a certain structure: for example, that it is a parallel composite of subsystems. This work consolidates, extends and improves upon aspects of earlier work of ours in this area. An extended example, consisting of a semantics for a simple parallel programming language, indicates a connection with separating logics for concurrency.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 19 , Issue 5 , October 2009 , pp. 959 - 1027
Copyright
Copyright © Cambridge University Press 2009

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Baeten, J. (2005) A brief history of process algebra. Theoretical Computer Science 335 (2-3)131–146.CrossRefGoogle Scholar
Ben-Ari, M. (1990) Principles of Concurrent and Distributed Programming, Prentice Hall.Google Scholar
Biri, N. and Galmiche, D. (2007) Models and separation logics for resource trees. Journal of Logic and Computation 17 (4)687–726.CrossRefGoogle Scholar
Birtwistle, G. (1979) Demos – discrete event modelling on Simula, Macmillan.CrossRefGoogle Scholar
Birtwistle, G., Pooley, R. and Tofts, C. (1993) Characterising the structure of simulations using CCS. Transactions of the Simulation Society 10 (3)205–236.Google Scholar
Birtwistle, G. and Tofts, C. (2001a) Getting Demos models right. (i). Practice. Simulation Practice and Theory 8 (6-7)377–393.CrossRefGoogle Scholar
Birtwistle, G. and Tofts, C. (2001b) Getting Demos models right. (ii) . . . and theory. Simulation Practice and Theory 8 (6-7)395–414.CrossRefGoogle Scholar
Calcagno, C., Gardner, P. and Zarfaty, U. (2005) Context logic and tree update. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages 2005 (POPL) 271–282.Google Scholar
Cardelli, L. and Gordon, A. (1998) Mobile ambients. In Nivat, M. (ed.) Foundations of Software Science and Computational Structures. Springer-Verlag Lecture Notes in Computer Science 1378 40–155.Google Scholar
Cleaveland, R., Parrow, J. and Steffen, B. (1993) The Concurrency Workbench: a semantics based tool for the verification of concurrent systems. In ACM Transactions on Programming Languages and Systems 15 36–72.CrossRefGoogle Scholar
Collinson, M., Pym, D. and Robinson, E. (2008) Bunched Polymorphism. Mathematical Structures in Computer Science 18 1091–1132.CrossRefGoogle Scholar
Collinson, M., Pym, D. and Tofts, C. (2007) Errata for Formal Aspects of Computing (2006) 18 495–517 and their consequences. Formal Aspects of Computing 19 (4)551–554.CrossRefGoogle Scholar
Conforti, G., Macedonio, D. and Sassone, V. (2007) Static bilog: a unifying language for spatial structures. Fundamenta Informaticae 80 1–20.Google Scholar
Dahl, O.-J., Myhrhaug, B. and Nygaard, K. (1970) Simula 67 Common Base Language. NCC Publication S-52, Norwegian Computing Center, Oslo.Google Scholar
Day, B. (1970) On closed categories of functors. In Proceedings of the Midwest Category Seminar. Springer-Verlag Lecture Notes in Mathematics 137.Google Scholar
Day, B. (1973) An embedding theorem for closed categories. In: Proceedings of the Sydney Category Seminar 1972/73. Springer-Verlag Lecture Notes in Mathematics 420.Google Scholar
Demos 2k Team (2002) Demos 2000. http://www.demos2k.org.Google Scholar
de Simone, R. (1985) Higher-level synchronising devices in Meije-SCCS. Theoretical Computer Science 37 245–267.CrossRefGoogle Scholar
Hennessy, M. and Milner, R. (1985) Algebraic laws for nondeterminism and concurrency. Journal of the ACM 32 (1)137–161.CrossRefGoogle Scholar
Hildebrandt, T. (1999) A Fully Abstract Presheaf Semantics of SCCS with Finite Delay. In: Proceedings of CTCS'99. Electronic Notes in Theoretical Computer Science 29.CrossRefGoogle Scholar
Hinton, A., Kwiatkowska, M., Norman, G. and Parker, D. (2006) Prism: A tool for automatic verification of probabilistic systems. In: Hermanns, H. and Palsberg, J. (eds.) Proc. 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'06). Springer-Verlag Lecture Notes in Computer Science 3920 441–444.Google Scholar
Hoyrup, M. (2007) Dynamical systems: stability and simulability. Mathematical Structures in Computer Science 17 (2)247–259.Google Scholar
Ishtiaq, S. and O'Hearn, P. (2001) BI as an assertion language for mutable data structures. In: Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages 2001 (POPL), London 14–26.CrossRefGoogle Scholar
Joyal, A., Nielsen, M. and Winskel, G. (1996) Bisimulation from open maps. Information and Computation 127 164–185.CrossRefGoogle Scholar
Kripke, S. (1963) Semantical analysis of modal logic I. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 9 67–96.Google Scholar
Kripke, S. (1965) Semantical analysis of intutionistic logic I. In: Crossley, J. and Dummett, M. (eds.) Formal Systems and Recursive Functions, Studies in Logic and the Foundations of Mathematics, North-Holland 92–130.Google Scholar
Lawvere, F. (1969) Adjointness in foundations. Dialectica 23 281–296.Google Scholar
Leifer, J. J. and Milner, R. (2000) Deriving bisimulation congruences for reactive systems. In: Proc. CONCUR 2000. Springer-Verlag Lecture Notes in Computer Science 1877.Google Scholar
Milner, R. (1980) A Calculus of Communicating Systems. Springer-Verlag Lecture Notes in Computer Science 92.Google Scholar
Milner, R. (1983) Calculi for synchrony and asynchrony. Theoretical Computer Science 25 267–310.CrossRefGoogle Scholar
Milner, R. (1989) Communication and Concurrency, Prentice-Hall.Google Scholar
Milner, R. (1999) Communicating systems and the π-calculus, Cambridge University Press.Google Scholar
O'Hearn, P. (2007) Resources, concurrency and local reasoning. Theoretical Computer Science 375 (1-3)271–307.CrossRefGoogle Scholar
O'Hearn, P. and Pym, D. (1999) The logic of bunched implications. Bulletin of Symbolic Logic 5 (2)215–244.Google Scholar
Plotkin, G. (2004) Structural operational semantics. Journal of Logic and Algebraic Programming 60 17–139. (Original unpublished manuscript 1981.)Google Scholar
Popkorn, S. (1994) First Steps in Modal Logic, Cambridge University Press.CrossRefGoogle Scholar
Pym, D. (1999) On bunched predicate logic. In: Proceedings of the 14th Symposium on Logic in Computer Science (LICS99), Trento, Italy, IEEE Computer Society Press 183–192.Google Scholar
Pym, D. (2002) The Semantics and Proof Theory of the Logic of Bunched Implications, Applied Logic Series 26, Kluwer Academic Publishers. (Errata at: http://www.cs.bath.ac.uk/~pym/BI-monograph-errata.pdf.)CrossRefGoogle Scholar
Pym, D., O'Hearn, P. and Yang, H. (2004) Possible worlds and resources: The semantics of BI. Theoretical Computer Science 315 (1)257–305.Google Scholar
Pym, D. and Tofts, C. (2006) A calculus and logic of resources and processes. Formal Aspects of Computing 18 (4)495–517. (Errata available: http://www.cs.bath.ac.uk/~pym/pym-tofts-fac-errata.pdf.)Google Scholar
Pym, D. and Tofts, C. (2007) Systems Modelling via Resources and Processes: Philosphy, Calculus, Semantics, and Logic. In: Cardelli, L., Fiore, M. and Winskel, G. (eds.) Computation, Meaning and Logic: articles dedicated to Gordon Plotkin. Electronic Notes in Theoretical Computer Science 172 545–587. (Errata at: http://www.cs.bath.ac.uk/~pym/pym-tofts-fac-errata.pdf.)Google Scholar
Reynolds, J. (2002) Separation logic: a logic for shared mutable data structures. In: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS02), Copenhagen, Denmark, IEEE Press 55–74.Google Scholar
Sassone, V. and Sobociński, P. (2003) Deriving bisimulation congruences using 2-categories. Nordic Journal of Computing 10 163–183.Google Scholar
Sewell, P. (1998) From rewrite rules to bisimulation congruences. Springer-Verlag Lecture Notes in Computer Science 1466 269–284.CrossRefGoogle Scholar
Stirling, C. (2001) Modal and temporal properties of processes, Springer-Verlag.Google Scholar
Tofts, C. (1994) Processes with probabilities, priority and time. Formal Aspects of Computing 6 536–564.Google Scholar
Tofts, C. (2006) Process algebra as modelling. In: Proceedings of the Workshop ‘Essays on Algebraic Process Calculi’ (APC25). Electronic Notes in Theoretical Computer Science 162 323–326.CrossRefGoogle Scholar
Victor, B. and Moller, F. (1994) The Mobility Workbench – a tool for the π-calculus. In: Dill, D. (ed.) CAV'94: Computer Aided Verification. Springer-Verlag Lecture Notes in Computer Science 818 428–440.Google Scholar
Winskel, G. and Nielsen, M. (1995) Models for concurrency. In: Handbook of Logic in Computer Science 4, Oxford University Press 1–148.Google Scholar