Dear Benjamin Lion, We regret to inform you that your paper 4841: Towards a Distributive Interpreter in Coq for Reactive Systems has not been accepted to FORMATS 2023. The quality of papers was very high, and many excellent papers were not able to be accepted. All papers received at least 3 reviews, which can be found below. We would like to thank you for your interest in FORMATS 2023, and hope that you will be able to attend the conference. Best wishes, Laure and Jeremy FORMATS 2023 PC chairs SUBMISSION: 4841 TITLE: Towards a Distributive Interpreter in Coq for Reactive Systems ----------------------- REVIEW 1 --------------------- SUBMISSION: 4841 TITLE: Towards a Distributive Interpreter in Coq for Reactive Systems AUTHORS: Benjamin Lion, David Nowak and Jean-Pierre Talpin ----------- Overall evaluation ----------- SCORE: -1 (weak reject) ----- TEXT: ===Summary=== The paper proposes to use comonads and monads to represent cyber-physical systems in Coq. The authors claim that it allows one to argue about the non-deterministic environment and the controller at the same time. ===Review= The paper is difficult to understand. It proposes to use an abstract theory to argue about concrete systems but falls short on clearly explaining the connection between the two. The term “monitoring” is well defined in the runtime verification community, but it is unclear if the authors are aware of this precisely. Presentation: The draft needs careful reading and polishing. It is missing a coherent flow of ideas. The abstract of the paper is misleading. The abstract states “Our goal is to design fully verified (safety-critical) programs…”, whereas it mentions monitoring several times, but the material presented is not about monitors. The first example is missing an explanation. It seems like it reads a sensor value and then triggers an actuator corresponding to that value if it is higher than a bound. The example is introduced with C for controller and P for (possibly) plant. Later, in table 2, two more processes are added: timer and A without much explanation. The paper jumps from one thing to another without clarifying the connections between the two. It talks about different things: monads and comonads, a term language, representing the processes as morphisms, composition of the processes, but leaves the task of bringing all these together to the reader. Technical contribution: I noticed that the proof that the compositions used in the paper satisfy axioms of a distributive law is left as future work. This exclusion should be justified. === Detailed Comments === Abstract, Line 7: What is the meaning of “deterministic” in brackets? Page 1, Introduction: the introduction starts rather abruptly and does not contain information about cyber-physical systems in practice. Does the actuator take a real value or a natural number? It is defined as a(n) but then executed as a(x) Columns in table 1 are referred before the table is referred. Table 1: t+ and t- are not defined. Furthermore, the purpose of this table is not entirely clear to me. I understand that it is supposed to be a motivation, but I do not understand in which way. The following two items do not necessarily require the table. The section on related work could put more emphasis on the difference between the described approaches and the proposed method. I would suggest introducing monads before comonads. Page 5 table 2: I would appreciate a longer description of the table as I do not think it is self explanatory. Page 5: P was referring to plant in the introduction, not it refers to plan. Is there a typo? Page 5, example 2: “St” does not seem to be defined or it is hard to find. It is clear that “S” is a state. Page 7, conclusion: the restriction mentioned in the conclusion is not addressed previously in the paper. It should be made clear that the proposed approach only considers stateless executions. === Minor Comments and Comments about Grammar === Introduction, Line 3: “real arithmetics” could probably be rephrased Introduction, Line 7: there should be a second punctuation mark after etc. Page 2, Line 1: there is a noun missing after “cyber-physical” “Can we infer a larger precision of x with additional readings?” Precisions are fine grained or coarse, or high or low, but not small or large. Page 3, paragraph 3: “hybrid monad as a semantic from imperative reactive programs”. Should the “from” be replaced by “for”? “However, such semantics is not operational”: is should be are. Page 3, contributions: “a categorical semantics” : the noun should either be singular or the article should be removed. Page 3, outline: “controller” should be plural and this also affects the verb in the relative clause. Page 4, second paragraph: “maybe monad” should probably be written in italic. Page 5, paragraph 1: “...and interprets such command by…” Command should be plural or an article is missing. “Finally, the real value are…” value should be plural or “are” should be “is”. Page 5, paragraph 2: “... and analyse invariant …”: “analyse” -> “analysing”, “invariant” -> “invariants” “effect of individual process” -> “processes” Page 5, section 3.1: What is the purpose of this section? From the title I would expect at least one definition. Page 6: “beteen” -> “between” Page 7, conclusion, first line: “result” should be plural. ----------- Recommended for artifact evaluation? ----------- no ----------------------- REVIEW 2 --------------------- SUBMISSION: 4841 TITLE: Towards a Distributive Interpreter in Coq for Reactive Systems AUTHORS: Benjamin Lion, David Nowak and Jean-Pierre Talpin ----------- Overall evaluation ----------- SCORE: 0 (borderline paper) ----- TEXT: This short paper proposes a language for describing programs with cyber-physical effects and equips it with categorical semantics. The proposed formalization of the problem has two advantages. First, the categorical semantics can be formalized in a proof assistant such as Coq, which can be then used to reason about the system properties and hence help the certification of the control program. It also provides compositional semantics (combining the monads for the effect of executions and comonads for the streaming of values) that are helpful for the monitoring tasks, where the monitoring is seen as a transformation of streams into streams. On the positive side, the paper proposes a new way to define controllers in the context of cyber-physical systems, which to my knowledge has not been much explored in the literature before. The topic of the paper fits well to the general FORMATS topics of interest (foundations and semantics), as well as the special track. I am not sure how much a typical FORMATS audience is familiar with category theory (I am not), and the paper is at times difficult to follow for non-experts. I understand that it is not possible to provide the full background in a short paper, but a very concrete running example (with a simple system such as a water tank composed with a simple environment) would help a lot following the details of the paper. The example provided in the paper is way too abstract to fully appreciate the value of the proposed framework. I would also appreciate some more information about the expressiveness of the proposed language, and how it compares to other formalisms for describing control programs. In particular, I would appreciate more information about the a(n) construct, and what kind of actuation it can model. Section 4 Implementation: ... as shown in 2 -> do you mean Table 2? ----------- Recommended for artifact evaluation? ----------- No necessarily. ----------------------- REVIEW 3 --------------------- SUBMISSION: 4841 TITLE: Towards a Distributive Interpreter in Coq for Reactive Systems AUTHORS: Benjamin Lion, David Nowak and Jean-Pierre Talpin ----------- Overall evaluation ----------- SCORE: 0 (borderline paper) ----- TEXT: The paper presents a formal framework for the description of cyber-physical systems based on categorical notions and the use of the Coq proof assistant. The paper presents the required notions from category theory, explains the perspective of a CPS as transforming input streams to output streams, obtained as a composition of processes (controller, timer, plant, approximation), and reasons about a simple language for CPSs in terms of this context. The paper also provides some details concerning proving invariants using Coq. The paper provides a good basis for future work. However the contribution of the paper in its current form seems too preliminary to warrant publication. In particular Section 4 requires further expansion and details; as it stands, the paper sets up its approach and then does not provide evidence that such an approach is actually useful. Further comments: - I appreciated the related work section, but I feel that the paper could be strengthened further by highlighting more clearly the benefit from following the paper's approach rather than adopting existing methods. - Section 2 could benefit from further explanation to help readers unfamiliar with categorical notions (of which there may be many in the FORMATS audience). In particular, the notions of "context-dependent" and "effectful" computations should be explained further. - There is to be a mismatch with how "monitoring" is used typically in the FORMATS (and not only) community and how it is meant here. Overall the approach of the paper is essentially verification. Typos and other minor comments: - Abstract: Remove the parentheses around "deterministic". "as a mean" --> "as a means" "until": incorrect use (means "while"?). - Introduction: "The recent exploration": the associated citation is from 2005. "cyber-physical would": missing a word. Hybrid automata should be mentioned as a formalism for CPSs. Please note that there are other ways to think of composition in this context: not just the composition of the controller with its environment, but also the composition of sub-modules of the controller. - Section 3: "The plan P" -> "The plant P" "analyse invariant on the system behavior": this concept should be clarified, perhaps with an example. "As explain in" -> "As explained in" It seems that I and St are single valuations, not sets. Also, I missed what D_\mathcal{S} and D_{St} are. - Section 4: "the prove" -> "the proof" "as shown in 2" -> "as shown in Section 2" ----------- Recommended for artifact evaluation? ----------- No