Conference Papers

  • 1. Ribeiro, P., Cavalcanti, A.: Angelic Processes for CSP via the UTP. Theoretical Computer Science. (2018).

    Demonic and angelic nondeterminism play fundamental roles as abstraction mechanisms for formal modelling. In contrast with its demonic counterpart, in an angelic choice failure is avoided whenever possible. Although it has been extensively studied in refinement calculi, in the context of process algebras, and of the Communicating Sequential Processes (CSP) algebra for refinement, in particular, it has been elusive. We show here that a semantics for an extended version of CSP that includes both demonic and angelic choice can be provided using Hoare and He’s Unifying Theories of Programming (UTP). Since CSP is given semantics in the UTP via reactive designs (pre and postcondition pairs) we have developed a theory of angelic designs and a conservative extension of the CSP theory using reactive angelic designs. To characterise angelic nondeterminism appropriately in an algebra of processes, however, a notion of divergence that can undo the history of events needs to be considered. Taking this view, we present a model for CSP where angelic choice completely avoids divergence just like in the refinement calculi for sequential programs.

    @article{Ribeiro2018,
      title = {Angelic Processes for {CSP} via the {UTP}},
      journal = {Theoretical Computer Science},
      year = {2018},
      issn = {0304-3975},
      doi = {10.1016/j.tcs.2018.10.008},
      url = {http://www.sciencedirect.com/science/article/pii/S0304397518306133},
      author = {Ribeiro, Pedro and Cavalcanti, Ana},
      keywords = {Semantics, formal specification, process algebras, CSP, UTP}
    }
    
  • 2. W. Li, A. Miyazawa, P. Ribeiro, A. L. C. Cavalcanti, J. C. P. Woodcock, J. Timmis: From formalised state machines to implementation of robotic controllers. In: Groß, R., Kolling, A., Berman, S., Frazzoli, E., Martinoli, A., Matsuno, F., and Gauci, M. (eds.) Distributed Autonomous Robotic Systems: The 13th International Symposium. pp. 517–529. Springer International Publishing (2018).
    @inbook{Li-etal2016,
      title = {From formalised state machines to implementation of robotic controllers},
      author = {W.~Li and A.~Miyazawa and P.~Ribeiro and A.~L.~C.~Cavalcanti and J.~C.~P.~Woodcock and J.~Timmis},
      booktitle = {Distributed Autonomous Robotic Systems: The 13th International Symposium},
      year = {2018},
      pages = {517--529},
      doi = {10.1007/978-3-319-73008-0_36},
      isbn = {978-3-319-73008-0},
      series = {Springer Tracts in Advanced Robotics},
      publisher = {Springer International Publishing},
      editor = {Gro{\ss}, Roderich and Kolling, Andreas and Berman, Spring and Frazzoli, Emilio and Martinoli, Alcherio and Matsuno, Fumitoshi and Gauci, Melvin"},
      url = {https://arxiv.org/abs/1702.01783}
    }
    
  • 3. P. Ribeiro, A. Miyazawa, W. Li, A. L. C. Cavalcanti, J. Timmis: Modelling and Verification of Timed Robotic Controllers. In: N. Polikarpova and S. Schneider (eds.) Integrated Formal Methods. pp. 18–33. Springer (2017).
    @inproceedings{Ribeiro2017,
      author = {P.~Ribeiro and A.~Miyazawa and W.~Li and A.~L.~C.~Cavalcanti and J.~Timmis},
      editor = {N.~Polikarpova and S.~Schneider},
      title = {Modelling and Verification of Timed Robotic Controllers},
      booktitle = {Integrated Formal Methods},
      year = {2017},
      publisher = {Springer},
      pages = {18--33},
      doi = {10.1007/978-3-319-66845-1_2},
      url = {https://www-users.cs.york.ac.uk/%7Ealcc/publications/papers/RMLCT17.pdf},
      isbn = {978-3-319-66845-1}
    }
    
  • 4. A. Miyazawa, P. Ribeiro, W. Li, A. L. C. Cavalcanti, J. Timmis: Automatic Property Checking of Robotic Applications. In: The International Conference on Intelligent Robots and Systems. pp. 3869–3876 (2017).
    @inproceedings{MRLCT17,
      author = {A.~Miyazawa and P.~Ribeiro and W.~Li and A.~L.~C.~Cavalcanti and J.~Timmis},
      title = {Automatic Property Checking of Robotic Applications},
      year = {2017},
      booktitle = {The International Conference on Intelligent Robots and Systems},
      pages = {3869-3876},
      doi = {10.1109/IROS.2017.8206238}
    }
    
  • 5. Ribeiro, P., Cavalcanti, A., Woodcock, J.: A Stepwise Approach to Linking Theories. In: Unifying Theories of Programming. Springer International Publishing (2016).

    Formal modelling of complex systems requires catering for a variety of aspects. The Unifying Theories of Programming (UTP) distinguishes itself as a semantic framework that promotes unification of results across different modelling paradigms via linking functions. The naive composition of theories, however, may yield unexpected or undesirable semantic models. Here, we propose a stepwise approach to linking theories where we deal separately with the definition of the relation between the variables in the different theories and the identification of healthiness conditions. We explore this approach by deriving healthiness conditions for Circus Time via calculation, based on the healthiness conditions of CSP and a small set of principles underlying the timed model.

    @incollection{Ribeiro2016,
      title = {{A} {S}tepwise {A}pproach to {L}inking {T}heories},
      author = {Ribeiro, P. and Cavalcanti, A. and Woodcock, J.},
      booktitle = {{U}nifying {T}heories of {P}rogramming},
      publisher = {Springer International Publishing},
      year = {2016},
      note = {(to appear)},
      series = {{L}ecture {N}otes in {C}omputer {S}cience},
      owner = {wv8579},
      timestamp = {2016.08.09}
    }
    
  • 6. Ribeiro, P., Cavalcanti, A.: Angelicism in the Theory of Reactive Processes. In: Naumann, D. (ed.) Unifying Theories of Programming. pp. 42–61. Springer International Publishing (2015).

    The concept of angelic nondeterminism has traditionally been employed in the refinement calculus. Despite different notions having been proposed in the context of process algebras, namely Communicating Sequential Processes (CSP), the analogous counterpart to the angelic choice operator of the monotonic predicate transformers, has been elusive. In order to consider this concept in the context of reactive processes, we introduce a new theory in the setting of Hoare and He’s Unifying Theories of Programming (UTP). Based on a theory of designs with angelic nondeterminism previously developed, we show how these processes can be similarly expressed as reactive designs. Furthermore, a Galois connection is established with the existing theory of reactive processes and a bijection is also found with respect to the subset of non-angelic processes.

    @incollection{Ribeiro2014,
      title = {{A}ngelicism in the {T}heory of {R}eactive {P}rocesses},
      author = {Ribeiro, Pedro and Cavalcanti, Ana},
      booktitle = {{U}nifying {T}heories of {P}rogramming},
      publisher = {Springer International Publishing},
      year = {2015},
      editor = {Naumann, David},
      pages = {42-61},
      series = {{L}ecture {N}otes in {C}omputer {S}cience},
      volume = {8963},
      doi = {10.1007/978-3-319-14806-9_3},
      isbn = {978-3-642-35704-6},
      owner = {pfr500},
      timestamp = {2014.06.05}
    }
    
  • 7. Ribeiro, P., Cavalcanti, A.: UTP Designs for Binary Multirelations. In: Ciobanu, G. and Méry, D. (eds.) Theoretical Aspects of Computing ICTAC 2014. pp. 388–405. Springer International Publishing (2014).

    The total correctness of sequential computations can be established through different isomorphic models, such as monotonic predicate transformers and binary multirelations, where both angelic and demonic nondeterminism are captured. Assertional models can also be used to characterise process algebras: in Hoare and He’s Unifying Theories of Programming, CSP processes can be specified as the range of a healthiness condition over designs, which are pre and postcondition pairs. In this context, we have previously developed a theory of angelic designs that is a stepping stone for the natural extension of the concept of angelic nondeterminism to the theory of CSP. In this paper we present an extended model of upward-closed binary multirelations that is isomorphic to angelic designs. This is a richer model than that of standard binary multirelations, in that we admit preconditions that rely on later or final observations as required for a treatment of processes.

    @incollection{Ribeiro2014a,
      title = {{UTP} {D}esigns for {B}inary {M}ultirelations},
      author = {Ribeiro, Pedro and Cavalcanti, Ana},
      booktitle = {{T}heoretical {A}spects of {C}omputing {ICTAC} 2014},
      publisher = {Springer International Publishing},
      year = {2014},
      editor = {Ciobanu, Gabriel and M\'{e}ry, Dominique},
      pages = {388-405},
      series = {{L}ecture {N}otes in {C}omputer {S}cience},
      volume = {8687},
      doi = {10.1007/978-3-319-10882-7_23},
      isbn = {978-3-642-39717-2},
      owner = {pfr500},
      timestamp = {2014.07.04}
    }
    
  • 8. Ribeiro, P., Cavalcanti, A.: Designs with Angelic Nondeterminism. In: Theoretical Aspects of Software Engineering (TASE), 2013 International Symposium on. pp. 71–78. IEEE (2013).

    Hoare and He’s Unifying Theories of Programming (UTP) are a predicative relational framework for the definition and combination of refinement languages for a variety of programming paradigms. Previous work has defined a theory for angelic nondeterminism in the UTP; this is basically an encoding of binary multirelations in a predicative model. In the UTP a theory of designs (pre and postcondition pairs) provides, not only a model of terminating programs, but also a stepping stone to define a theory for state-rich reactive processes. In this paper, we cast the angelic nondeterminism theory of the UTP as a theory of designs with the long-term objective of providing a model for well established refinement process algebras like Communicating Sequential Processes (CSP) and Circus.

    @inproceedings{Ribeiro2013,
      title = {{D}esigns with {A}ngelic {N}ondeterminism},
      author = {Ribeiro, P. and Cavalcanti, A.},
      booktitle = {{T}heoretical {A}spects of {S}oftware {E}ngineering ({TASE}), 2013 {I}nternational {S}ymposium on},
      year = {2013},
      pages = {71-78},
      publisher = {IEEE},
      doi = {10.1109/TASE.2013.18},
      keywords = {communicating sequential processes;formal specification;program verification;refinement calculus;relational algebra;CSP;Circus;UTP;Unifying Theories of Programming;angelic nondeterminism theory;binary multirelation encoding;communicating sequential process;predicative model;predicative relational framework;program termination;programming paradigm;refinement language;refinement process algebra;state-rich reactive process;Algebra;Educational institutions;Electronic mail;Encoding;Lattices;Programming},
      owner = {pfr},
      timestamp = {2013.12.06}
    }
    

Technical Reports

  • 1. Ribeiro, P.: Super-Theories. University of York (2016).
    @techreport{Ribeiro2016a,
      title = {{S}uper-{T}heories},
      author = {Ribeiro, Pedro},
      institution = {University of York},
      year = {2016},
      note = {\url{https://www-users.cs.york.ac.uk/pfr/reports/super-theories.pdf}},
      owner = {wv8579},
      timestamp = {2016.03.08},
      url = {https://www-users.cs.york.ac.uk/pfr/reports/super-theories.pdf}
    }
    
  • 2. Ribeiro, P.: Reactive angelic processes. University of York (2014).
    @techreport{Ribeiro2013a,
      title = {{R}eactive angelic processes},
      author = {Ribeiro, Pedro},
      institution = {University of York},
      year = {2014},
      month = feb,
      note = {http://www-users.cs.york.ac.uk/pfr/reports/rac.pdf},
      type = {{T}echnical report},
      owner = {pfr500},
      timestamp = {2013.12.12},
      url = {http://www-users.cs.york.ac.uk/pfr/reports/rac.pdf}
    }
    
  • 3. Ribeiro, P.: Designs with Angelic Nondeterminism. University of York (2013).
    @techreport{Ribeiro2013b,
      title = {{D}esigns with {A}ngelic {N}ondeterminism},
      author = {Ribeiro, Pedro},
      institution = {University of York},
      year = {2013},
      month = feb,
      note = {http://www-users.cs.york.ac.uk/pfr/reports/dac.pdf},
      type = {{T}echnical {R}eport},
      owner = {pfr},
      timestamp = {2013.02.07},
      url = {http://www-users.cs.york.ac.uk/pfr/reports/dac.pdf}
    }
    

Thesis

  • 1. Ribeiro, P.: Angelic Processes, http://arxiv.org/abs/1505.04726, (2014).
    @phdthesis{RibeiroT2014,
      title = {{A}ngelic {P}rocesses},
      author = {Ribeiro, P.},
      school = {University of York},
      year = {2014},
      month = dec,
      type = {{P}h.{D}. dissertation (extended version)},
      owner = {pfr500},
      timestamp = {2014.11.05},
      url = {http://arxiv.org/abs/1505.04726}
    }
    
  • 2. Ribeiro, P.: Angelic Processes, http://etheses.whiterose.ac.uk/9020/, (2014).
    @phdthesis{RibeiroT2014b,
      title = {{A}ngelic {P}rocesses},
      author = {Ribeiro, P.},
      school = {University of York},
      year = {2014},
      month = dec,
      note = {http://etheses.whiterose.ac.uk/9020/},
      type = {{Ph.D} thesis},
      owner = {wv8579},
      timestamp = {2015.07.26},
      url = {http://etheses.whiterose.ac.uk/9020/}
    }