%0 Conference Proceedings %T A Calculus of Virtually Timed Ambients %+ University of Oslo (UiO) %A Johnsen, Einar, Broch %A Steffen, Martin %A Stumpf, Johanna, Beate %Z Part 4: Regular Papers %< avec comité de lecture %( Lecture Notes in Computer Science %B 23th International Workshop on Algebraic Development Techniques (WADT) %C Gregynog, United Kingdom %Y Phillip James %Y Markus Roggenbach %I Springer International Publishing %3 Recent Trends in Algebraic Development Techniques %V LNCS-10644 %P 88-103 %8 2016-09-21 %D 2016 %R 10.1007/978-3-319-72044-9_7 %Z Computer Science [cs]Conference papers %X A virtual machine, which is a software layer representing an execution environment, can be placed inside another virtual machine. As virtual machines at every level in a location hierarchy compete with other processes for processing time, the computing power of a virtual machine depends on its position in this hierarchy and may change if the virtual machine moves. These effects of nested virtualization motivate the calculus of virtually timed ambients, a formal model of hierarchical locations for execution with explicit resource provisioning, introduced in this paper. Resource provisioning in this model is based on virtual time slices as a local resource. To reason about timed behavior in this setting, weak timed bisimulation for virtually timed ambients is defined as an extension of bisimulation for mobile ambients. We show that the equivalence of contextual bisimulation and reduction barbed congruence is preserved by weak timed bisimulation. The calculus of virtually timed ambients is illustrated by examples. %G English %Z TC 1 %Z WG 1.3 %2 https://inria.hal.science/hal-01767462/document %2 https://inria.hal.science/hal-01767462/file/433330_1_En_7_Chapter.pdf %L hal-01767462 %U https://inria.hal.science/hal-01767462 %~ IFIP-LNCS %~ IFIP %~ IFIP-TC %~ IFIP-TC1 %~ IFIP-WG1-3 %~ IFIP-WADT %~ IFIP-LNCS-10644