Timed mobility in process algebra and Petri nets (Q638567)

A process algebra called TiMo (timed mobility) is presented. It can express both explicit locations in a distributed environment and various timed constraints (timeouts of interactions, i.e., inputs and outputs and migrations from one location to another). The model of time is based on local clocks (visible only to local processes). An operational semantics for TiMo is given by structural equivalence and operational semantics rules. There are two kinds of rules -- one for action executions and another for a unit time progression. A structural translation of TiMo into behaviorally equivalent high-level timed Petri nets is provided (with the help of a net algebra). In this way a formal net semantics for timed interaction and migration which is both structural and allows to directly deal with concurrency and causality is obtained.