HpC: A Calculus for Hybrid and Mobile Systems -- Full Version

Bohua Zhan; Hao Wu; Jean-Pierre Talpin; Naijun Zhan; Shuling Wang; Xinxin Liu; Xiong Xu

REVIEW 4 major objections 5 minor 12 references

HpC: A Calculus for Hybrid and Mobile Systems -- Full Version

T0 review · 4 major / 5 minor · reviewed 2026-08-10 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read The paper introduces HpC, a conservative extension of the π-calculus in which continuous ODE evolution and channel mobility coexist, and proves a train handover protocol is approximately bisimilar to a disturbance-free specification…

desk verdict A genuinely new hybrid pi-calculus with a real case study, but the approximate-bisimulation definition is too weak to deliver the claimed control-theoretic guarantee. read the letter →

arxiv 2501.09430 v1 pith:HHCCTDNF submitted 2025-01-16 cs.PL cs.LOcs.NIcs.SYeess.SY

Xiong Xu , Jean-Pierre Talpin , Shuling Wang , Hao Wu , Bohua Zhan , Xinxin Liu , Naijun Zhan This is my paper · ORCID

classification cs.PLcs.LOcs.NIcs.SYeess.SY MSC 68Q8568Q6093C30

keywords hybridpi-calculusapproximatebisimulationprocesscalculusmobilitysystemsoperationalsemanticsbarriercertificatestrainhandoverprotocol

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper introduces HpC, a hybrid extension of the classical $\pi$-calculus in which continuous variables, channels, and processes are all first-class names and every process has both discrete and continuous operational semantics. The authors claim this extension is conservative and minimal, so the standard theory of bisimulation and congruence lifts unchanged from the $\pi$-calculus. The central verified result is that a train-control handover protocol under bounded disturbance is approximately bisimilar to an ideal three-stage specification: the two systems' positions never diverge by more than 0.4 km (and 0.3 km in the failed-handover scenario). If the claim holds, HpC gives a process-algebraic route to proving bounded-distance correctness for mobile, hybrid, and networked IoT systems.

What carries the argument

The central object is the continuous prefix $\{\vec{x}_0 \mid \dot{\vec{x}}=\vec{f}\ \&\ \varphi, R\}(\vec{y}).P$ with its flow semantics: a flow $\alpha\cdot\gamma$ (assumption·guarantee) records the trajectory of the process's own variables as the guarantee and the environment's variables as the assumption, and the ready set $R$ declares which channel names can be sensed or actuated during evolution. Parallel composition composes flows like contracts and forbids simultaneous waiting on dual channels, forcing a discrete handshake instead. The argument for the case study is carried by reducing approximate bisimulation of the two systems to safety of a composed hybrid automaton, then proving that safety by a differential invariant (barrier certificate): a linear certificate $b = 0.12386\,x_1 + 0.60533\,v_1 - 0.00588\,a_1 - 8.19308\,t_1 + 0.12017\,x_2 + 0.58482\,v_2 - 0.03074\,a_2 + 0.64709\,t_2 - 0.40900$ gives $|x_1-x_2|\le 0.4\,\mathrm{km}$ for all trajectories.

What would settle it

Simulate the composed hybrid automaton of the case study under a disturbance $D$ that stays within the assumed bound $[-0.1,0.1]$ and a control period of 1 s, and measure $\max |x_{\mathrm{SPEC}} - x_{\mathrm{System}}|$ over all runs; the paper reports about 0.205 km, so any run exceeding 0.4 km would refute Proposition 7.1. Alternatively, apply Definition 6.6 directly to two processes that start 0.2 km apart, take the same total time, but diverge by 1 km in the middle—such a pair would be (0.2 km, 0)-approximately bisimilar on the definition as written, exposing that the definition does not enforce pointwise closeness.

Watch

Extended reading notes

Core claim

The paper's core discovery is that a $\pi$-calculus can be extended with ordinary differential equations and with sensing/actuation interfaces—without changing the name-first philosophy—so that hybrid and mobile behaviour live in one calculus. In HpC, a continuous process is written as a prefix $\{\vec{x}_0 \mid \dot{\vec{x}}=\vec{f}\ \&\ \varphi, R\}(\vec{y}).P$, where the ODE evolves from $\vec{x}_0$ until the boundary condition $\varphi$ fails, while channels in the ready set $R$ can interrupt the flow for discrete input or output. The operational semantics gives every process both discrete transitions and continuous transitions labelled by a flow (an assumption·guarantee pair) and a ready set, and the paper proves that strong and weak bisimulation remain equivalence relations and congruences. On top of this, the paper defines a two-parameter approximate bisimulation, $\approx_{\eta,\varepsilon}$, which matches a continuous transition by a sequence of continuous transitions whose total duration is within $\varepsilon$ and whose first left-states are within $\eta$. The case study proves $\mathrm{SPEC} \approx_{0.4\mathrm{km},0} \mathrm{System}$ and $\mathrm{SPEC}_0 \approx_{0.3\mathrm{km},0} \mathrm{System}_0$ for the train handover protocol, using a barrier-certificate invariant to show the distance between the two positions stays bounded.

Load-bearing premise

In Definition 6.6, for a continuous transition of one side the other side only needs to start within $\eta$ and match the total duration up to $\varepsilon$; it does not have to stay close to the first system in between or at the end, so the approximate bisimulation relation alone does not supply the usual "all states remain close" guarantee.

Editorial extensions

If this is right

The Discretisation Theorem (6.7) lets a continuous ODE be replaced by a sampling process using Runge-Kutta steps while preserving an $(\eta,\varepsilon)$-approximate bisimulation, so verified hybrid models can be compiled to discrete controllers with a formal error bound.
Existing $\pi$-calculus results, including congruence and strong and weak bisimulation, transfer to HpC unchanged, so mobile-communication proofs can be reused in hybrid settings.
The handover-protocol proof pattern—specify an ideal model, add bounded disturbance, and certify a differential invariant—provides a template for verifying other safety-critical mobile CPS protocols, such as vehicle platooning or drone handoffs.
Since HpC treats physical variables as channels, a sector can hand over control of a train by sending the names of those variables over a servicing channel, so network topology and continuous physics evolve in one framework.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

An unstated corollary of the discretisation theorem is that Euler or adaptive-step integrators could be certified with the same two-parameter bisimulation, provided their local error bounds are established.
Because Definition 6.6 only requires initial-state closeness and total-duration tolerance, it may under-approximate the intuitive 'states stay close throughout' requirement; a strengthened definition with a pathwise distance bound would make the guarantee direct rather than an extra proof obligation.
The barrier-certificate invariant used in the case study suggests that controller parameters (sector length, handover point, control period, disturbance bound) could be synthesised by solving the certificate constraints, turning verification into a parameter design tool.
The same proof technique should extend to multiple trains and sectors, since the composition of the hybrid automata is per-location and the barrier certificate is computed location-wise.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

The paper delivers a real new calculus: HpC puts ODE flows, continuous names, and mobile channel passing under one roof, and the strong and weak bisimulation theory looks sound. The congruence proof is sketched rather than fully detailed, but the shape is standard and plausible. The train handover case study is substantial, and the authors actually run barrier-certificate synthesis and ship code for the numerical part. That is reproducible evidence, and it earns the paper a serious read.

The stress-test note is correct, and the reader's conditional verdict matches mine. Definition 6.6 only requires the left states of matched continuous transitions to be within eta and the total durations to be within epsilon. It never bounds the right states or the intermediate trajectory distance. So two processes can be (eta,epsilon)-approximately bisimilar even if their observable variables drift far apart during a continuous evolution and then come back. That is not the standard Girard-Pappas notion, which keeps a global state bound. The paper's headline claim to support 'control-theoretic approximate bisimulation' is therefore overstated. What saves Proposition 7.1 is not the definition: it is the separate barrier-certificate invariant showing |G1-G2| ≤ 0.4 km at all times. That invariant is exactly the missing closeness clause, and the proof would still work if the definition were repaired.

A second soft spot is the conservative-extension claim. It is asserted early and never given as a formal theorem with a proof. To make it stick, the authors need to show that the bisimulation theory on the pure pi-calculus fragment coincides with the classical one. That is probably true, but it is not established here.

In proportion: these are addressable weaknesses in an otherwise strong paper. The calculus design, the strong/weak bisimulation framework, and the case study are contributions worth publishing. The approximate-bisimulation section needs reworking, not removal. I would send this to a serious referee and expect major revision, with the closeness condition added to Definition 6.6 and the conservative extension either proven or downgraded to 'extension'.

For the right reader — someone working on process calculi for hybrid systems or on verification of mobile cyber-physical systems — this is a paper to know about. I'd bring it to a reading group specifically to discuss the definitional fix.

Referee Report

4 major / 5 minor

Summary. The paper introduces HpC, an extension of the classical π-calculus with ordinary differential equations, Boolean guards, and 'continuous channels' as first-class names. It defines operational semantics for discrete and continuous transitions, then develops strong, weak, and approximate bisimulation relations for the calculus. The paper claims that HpC is a conservative extension of the π-calculus, that the bisimulation theory lifts to the hybrid setting, and that HpC is the first calculus to support control-theoretic approximate bisimulation in the presence of dynamic and mobile channels. The main verified result is Proposition 7.1, which states that a disturbed train handover system is (0.4 km, 0)-approximately bisimilar to an ideal specification, proved with the help of a barrier certificate on a composed hybrid automaton.

Significance. If the definitional and proof issues were resolved, this would be a useful contribution at the intersection of process calculi and hybrid systems verification: it combines name-passing mobility with continuous ODE dynamics and gives a concrete case study in which approximate behavioural equivalence is certified by a barrier certificate. The case study is nontrivial and the use of barrier certificates inside a process-calculus bisimulation proof is promising. However, the central notion of approximate bisimulation as stated does not deliver the advertised control-theoretic guarantee, and the proof of the headline proposition is only sketched. These issues must be addressed before the paper's main claims are supported.

major comments (4)

[Section 6.3, Definition 6.6] Definition 6.6 is not a control-theoretic approximate bisimulation in the standard sense of the Girard–Pappas notion cited in the related work. The last clause requires, for a continuous transition of P, that Q match with a sequence of continuous transitions whose first left state is within η and whose total duration differs by at most ε from P's flow. It never bounds the distance between the two systems' continuous states at intermediate times or at the end of the matched evolution, and the relation S itself carries no metric on the current values of continuous names. Consequently, two processes can be (η,ε)-approximately bisimilar while observable continuous variables drift arbitrarily far apart during a matched flow, as long as the residual processes are related. This directly undermines the Abstract and Section 1 claims that HpC 'supports control-theoretic approximate bisimulation'. The proof of Proposition 7.1 compensates by proving the stronger invariant |G1-G2| ≤ 0.4 km at all times via barrier certificates, but that invariant is not a consequence of Definition 6.6. The definition should be strengthened to require distance bounds at all relevant points of the matched trajectories, or the weaker notion should be explicitly named and the control-theoretic interpretation restricted accordingly.
[Section 7.6.7, Proposition 7.1] Proposition 7.1 is not proved from Definition 6.6. The relation S displayed in the proof is defined purely by reachability under continuous transitions with equal total duration; it does not include the η and ε side conditions, and the text gives no verification of the four bisimulation clauses for arbitrary pairs in S, no treatment of the abstraction/concretion matching for channel mobility, and no argument that the safety certificate on the composed automaton H implies the required matching transitions. The sentence 'We first prove that the distance ... is not larger than 0.4 km, based on which we then prove that the following relation forms a (0.4 km, 0)-approximate bisimulation' is a proof sketch rather than a proof. Appendix B provides the barrier certificate itself but not the lifting argument to the bisimulation clauses. Since Proposition 7.1 is the paper's main verified result, the proof must be spelled out in full, including a demonstration that the displayed relation indeed satisfies each condition of Definition 6.6.
[Section 6, opening paragraph; Abstract] The paper asserts that HpC is a conservative extension of the classical π-calculus and that the extension is 'minimal', allowing all theoretical results such as bisimulation to be lifted. No formal statement or proof of conservativity appears anywhere in the manuscript. In particular, there is no defined embedding of π-calculus processes into HpC, and no theorem establishing that π-calculus transitions and bisimilarity are preserved and reflected by that embedding. This is a load-bearing claim for the paper's framing as a 'conservative extension'. The authors should either provide a precise conservativity theorem with proof, or explicitly weaken the claim to state which results are inherited and in what sense.
[Section 6.3, Theorem 6.7] Theorem 6.7 states a discretisation result: given a locally Lipschitz ODE, its continuous evolution process is (η,δ)-approximately bisimilar to a Runge-Kutta step process, for any precision η above the initial error. No proof of this theorem is provided in the main text or in the appendices. The theorem is advertised as a bridge from HpC models to correct executable code, and its unproved status is a significant gap in a paper whose central contribution is the approximate bisimulation theory. The authors should either include a full proof or explicitly label the statement as a conjecture and adjust the claims made about it.

minor comments (5)

[Throughout] The symbol π is consistently rendered as 'c' in the text (e.g., 'hybrid c-calculus', 'c-calculus'), which appears to be an encoding or OCR artifact and makes the paper difficult to read.
[Section 7.6.7] In the definition of the relation S, the notation 'SPEC hd1,;i=>' is used without a preceding transition arrow; the paper should use the weak transition notation introduced in Section 6.2 consistently.
[Remark 3, Section 5.4.2] The remark writes 'hdd;,;i' for a zero-flow continuous action, but later uses 'hd,;i' and 'hd,;i' elsewhere; the notation should be made uniform.
[Section 7.6.7] The sentence 'By simulation, the maximum distance is around 0.205 km' reports an empirical value that is not used in the proof; either remove it or state clearly that it is informal and not part of the verified result.
[Section 1, related works] The citation to [59] as 'hybrid Hoare logic' is to an arXiv preprint; if a published version exists, it should be cited instead or in addition.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: HpC's calculus and bisimulation theory are derived from the LTS definitions, and Proposition 7.1 is proved by an independent barrier-certificate invariant rather than by assuming the conclusion.

full rationale

The paper's derivation chain is self-contained. Strong and weak bisimulation (Definitions 6.1 and 6.4) are standard LTS-based notions extended to continuous transitions; Theorem 6.3's congruence proof is carried out in Appendix A using candidate relations checked against the operational rules, not imported from the conclusion. Definition 6.6 introduces a new approximate-bisimulation relation with explicit tolerances (η, ε); it is not obtained by fitting a parameter to the case study. In Proposition 7.1, the candidate relation S is defined over reachable pairs of SPEC and System runs with equal total duration, and the proof then reduces the bisimulation obligation to a safety property of the composed automaton H. That safety property is established by a barrier certificate whose constraints (BC-1)-(BC-4) are stated and solved numerically; the certificate does not assume that SPEC ⇡(0.4km,0) System. The 0.4 km bound is a verified target, and the simulation remark that the maximum distance is about 0.205 km is an observation, not the proof input. Self-citations ([57], [58], [59], [53]) provide context or a control-curve formula that is fully written out in the paper, so they are not load-bearing. A genuine weakness, but not a circularity, is that Definition 6.6's continuous clause bounds only left states and total durations, not right states or intermediate distances; the stronger invariant |G1-G2| ≤ 0.4 km used in the proof of Proposition 7.1 is exactly what compensates for that gap. This is a soundness/correctness limitation of the proposed definition, not a case of the derivation reducing to its own inputs.

Assumptions & free parameters 1 free parameters · 4 assumptions · 0 invented entities

The central theoretical contribution rests on standard pi-calculus machinery and on the domain assumption that ODEs are locally Lipschitz and flows are right-continuous and semi-differentiable. The approximate bisimulation definition itself is an ad hoc-to-paper modeling choice that is load-bearing for the case study. No new physical entities are postulated; the SDP certificate search in Appendix B involves hand-chosen hyperparameters but these are proof-search parameters, not parameters of the theorem.

free parameters (1)

Barrier certificate SDP parameters W_4 and lambda = W_4 = 1, lambda = 0.25
Chosen by trial in Appendix B to obtain a certificate for the composed automaton. They are not physical constants, but they are hand-chosen to make the proof search succeed.

assumptions (4)

domain assumption ODE vector fields are locally Lipschitz continuous and admit unique solutions over the interval [0,d]
Stated in Section 4.2 and required by Theorem 6.7; used for existence and uniqueness of flows in the Run and Stop rules.
domain assumption Flows are right-continuous, semi-differentiable, and have left limits at endpoints
Section 5.3 imposes these conditions to define concatenation and limits used in the operational semantics.
standard math The discrete part of HpC inherits the standard pi-calculus semantics, including the theory of abstractions and concretions from Milner's work
Used throughout Section 5.4 and in the bisimulation proofs.
ad hoc to paper Approximate bisimulation as defined in Def. 6.6 is the intended notion of behavioural closeness; it assumes that matching initial left states and total durations suffices to guarantee approximate equivalence
This definitional choice is load-bearing for the case study; it is weaker than standard approximate bisimulation and is not justified by a theorem showing it implies closeness along trajectories.

how reviews work

0 comments

Cite this review

Pith. "Pith review of HpC: A Calculus for Hybrid and Mobile Systems -- Full Version." pith.science (2026). https://pith.science/paper/HHCCTDNF

@misc{pith2026250109430,
  author       = {Pith},
  title        = {Pith review of: HpC: A Calculus for Hybrid and Mobile Systems -- Full Version},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/HHCCTDNF}},
  note         = {Machine review of arXiv:2501.09430}
}

read the original abstract

Networked cybernetic and physical systems of the Internet of Things (IoT) immerse civilian and industrial infrastructures into an interconnected and dynamic web of hybrid and mobile devices. The key feature of such systems is the hybrid and tight coupling of mobile and pervasive discrete communications in a continuously evolving environment (discrete computations with predominant continuous dynamics). In the aim of ensuring the correctness and reliability of such heterogeneous infrastructures, we introduce the hybrid {\pi}-calculus (HpC), to formally capture both mobility, pervasiveness and hybridisation in infrastructures where the network topology and its communicating entities evolve continuously in the physical world. The {\pi}-calculus proposed by Robin Milner et al. is a process calculus that can model mobile communications and computations in a very elegant manner. The HpC we propose is a conservative extension of the classical {\pi}-calculus, i.e., the extension is ``minimal'', and yet describes mobility, time and physics of systems, while allowing to lift all theoretical results (e.g. bisimulation) to the context of that extension. We showcase the HpC by considering a realistic handover protocol among mobile devices.

Figures

Figures reproduced from arXiv: 2501.09430 by the authors.

**Figure 3.** The hybrid automata of SPEC (le!) and System (right) In order to observe the di"erence between the real-time positions (G) of the trains in SPEC and System, we compose the hybrid automata in [PITH_FULL_IMAGE:figures/full_fig_p024_3.png] view at source ↗

**Figure 4.** The composed hybrid automaton H The existence of the aforementioned di"erential invariant is established by using barrier certi!- cates [26, 43]. However, a detailed discussion of barrier certi$cates is beyond the scope of this paper. Appendix B provides formal de$nitions of hybrid automata and barrier certi$cates, along with an explanation of how to compute the desired di"erential invariant using these techniques. … view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

12 extracted references · 11 canonical work pages

[1]

Henzinger, and Pei-Hsin Ho

Rajeev Alur, Costas Courcoubetis, Thomas A. Henzinger, and Pei-Hsin Ho. 1992. Hybrid Automata: An Algorithmic Approach to the Specication and Verication of Hybrid Systems. In Hybrid Systems (LNCS, Vol. 736) . Springer, 209–229. [2]Bogdan Aman and Gabriel Ciobanu. 2013. Real-Time Migration Properties of rTiMo Veried in Uppaal. In SEFM 2013 (LNCS, Vol. 8...

work page 1997
[5]

Jos C. M. Baeten and Cornelis A. Middelburg. 2002. Process Algebra with Timing . Springer. [6]Richard Banach. 2024. Core Hybrid Event-B III: Fundamentals of a reasoning framework. Sci. Comput. Program. 231 (2024), 103002. [7]Richard Banach, Michael J. Butler, Shengchao Qin, Nitika Verma, and Huibiao Zhu. 2015. Core Hybrid Event-B I: Single Hybrid Event-B ...

work page 2024
[12]

Ningning Chen and Huibiao Zhu. 2023. A process calculus SMrCaIT for IoT. J. Softw. Evol. Process. (2023). [13]Xin Chen, Sriram Sankaranarayanan, and Erika Ábrahám. 2014. Under-approximate owpipes for non-linear continu- ous systems. In FMCAD 2014. IEEE, 59–66. [14]Gabriel Ciobanu and Maciej Koutny. 2011. Timed Mobility in process algebra and Petri nets. ...

work page 2023
[23]

Henzinger

Thomas A. Henzinger. 1996. The Theory of Hybrid Automata. In LICS 1996. IEEE Computer Society, 278–292

work page 1996
[24]

C. A. R. Hoare. 1978. Communicating Sequential Processes. Commun. ACM 21, 8 (1978), 666–677. [25]A. Agung Julius, Alessandro D’Innocenzo, Maria Domenica Di Benedetto, and George J. Pappas. 2009. Approximate equivalence and synchronization of metric transition systems. Syst. Control. Lett. 58, 2 (2009), 94–101. [26]Hui Kong, Fei He, Xiaoyu Song, William N....

work page 1978
[33]

MathWorks. 2013. Simulink®User’s Guide.http://www.mathworks.com/help/pdf_doc/simulink/sl_using.pdf

work page 2013
[34]

MathWorks. 2013. Stateow®User’s Guide.http://www.mathworks.com/help/pdf_doc/stateow/sf_ug.pdf

work page 2013
[35]

Robin Milner. 1993. The Polyadicc-Calculus: A Tutorial. Springer

work page 1993

Show all 12 references

[36]

Robin Milner. 1999. Communicating and Mobile Systems: the c-Calculus. Cambridge University Press. [37]Robin Milner, Joachim Parrow, and David Walker. 1992. A Calculus of Mobile Processes, I. Inf. Comput.100, 1 (1992), 1–40. [38]Robin Milner, Joachim Parrow, and David Walker. 1...

1992
[40]

André Platzer. 2008. Dierential Dynamic Logic for Hybrid Systems. J. Autom. Reason. 41, 2 (2008), 143–189

2008
[41]

André Platzer. 2012. The Complete Proof Theory of Hybrid Systems. In LICS. IEEE Computer Society, 541–550

2012
[42]

André Platzer. 2018. Logical Foundations of Cyber-Physical Systems . Springer. [43]Stephen Prajna and Ali Jadbabaie. 2004. Safety Verication of Hybrid Systems Using Barrier Certicates. In HSCC (LNCS, Vol. 2993). Springer, 477–492. [44]William C. Rounds. 2004. A Spatial Logic...

2019 arXiv

Pith tools

Reviewed August 10, 2026 · model on record in the stance chip above.

[1] [1]

Henzinger, and Pei-Hsin Ho

Rajeev Alur, Costas Courcoubetis, Thomas A. Henzinger, and Pei-Hsin Ho. 1992. Hybrid Automata: An Algorithmic Approach to the Specication and Verication of Hybrid Systems. In Hybrid Systems (LNCS, Vol. 736) . Springer, 209–229. [2]Bogdan Aman and Gabriel Ciobanu. 2013. Real-Time Migration Properties of rTiMo Veried in Uppaal. In SEFM 2013 (LNCS, Vol. 8...

work page 1997

[2] [5]

Jos C. M. Baeten and Cornelis A. Middelburg. 2002. Process Algebra with Timing . Springer. [6]Richard Banach. 2024. Core Hybrid Event-B III: Fundamentals of a reasoning framework. Sci. Comput. Program. 231 (2024), 103002. [7]Richard Banach, Michael J. Butler, Shengchao Qin, Nitika Verma, and Huibiao Zhu. 2015. Core Hybrid Event-B I: Single Hybrid Event-B ...

work page 2024

[3] [12]

Ningning Chen and Huibiao Zhu. 2023. A process calculus SMrCaIT for IoT. J. Softw. Evol. Process. (2023). [13]Xin Chen, Sriram Sankaranarayanan, and Erika Ábrahám. 2014. Under-approximate owpipes for non-linear continu- ous systems. In FMCAD 2014. IEEE, 59–66. [14]Gabriel Ciobanu and Maciej Koutny. 2011. Timed Mobility in process algebra and Petri nets. ...

work page 2023

[4] [23]

Henzinger

Thomas A. Henzinger. 1996. The Theory of Hybrid Automata. In LICS 1996. IEEE Computer Society, 278–292

work page 1996

[5] [24]

C. A. R. Hoare. 1978. Communicating Sequential Processes. Commun. ACM 21, 8 (1978), 666–677. [25]A. Agung Julius, Alessandro D’Innocenzo, Maria Domenica Di Benedetto, and George J. Pappas. 2009. Approximate equivalence and synchronization of metric transition systems. Syst. Control. Lett. 58, 2 (2009), 94–101. [26]Hui Kong, Fei He, Xiaoyu Song, William N....

work page 1978

[6] [33]

MathWorks. 2013. Simulink®User’s Guide.http://www.mathworks.com/help/pdf_doc/simulink/sl_using.pdf

work page 2013

[7] [34]

MathWorks. 2013. Stateow®User’s Guide.http://www.mathworks.com/help/pdf_doc/stateow/sf_ug.pdf

work page 2013

[8] [35]

Robin Milner. 1993. The Polyadicc-Calculus: A Tutorial. Springer

work page 1993