Wyniki wyszukiwania - BazTech

1

A Many-sorted Polyadic Modal Logic

Leuştean Ioana, Moangă Natalia, Şerbănuţă Traian Florin

Fundamenta Informaticae

|

2020

|

Vol. 173, nr 2-3

191--215

EN

We propose a general system that combines the powerful features of modal logic and many-sorted reasoning. Its algebraic semantics leads to a many-sorted generalization of boolean algebras with operators, for which we prove the analogue of the Jónsson-Tarski theorem. Our goal was to deepen the connections between modal logic and program verification, while also testing the expressiveness of our system by defining a small imperative language and its operational semantics.

2

A Formal, Resource Consumption-Preserving Translation from Actors with Cooperative Scheduling to Haskell

Albert Elvira, Bezirgiannis Nikolaos, de Boer Frank, Martin-Martin Enrique

Fundamenta Informaticae

|

2020

|

Vol. 177, nr 3/4

203--234

EN

We present a formal translation of a resource-aware extension of the Abstract Behavioral Specification (ABS) language to the functional language Haskell. ABS is an actor-based language tailored to the modeling of distributed systems. It combines asynchronous method calls with a suspend and resume mode of execution of the method invocations. To cater for the resulting cooperative scheduling of the method invocations of an actor, the translation exploits for the compilation of ABS methods Haskell functions with continuations. The main result of this article is a correctness proof of the translation by means of a simulation relation between a formal semantics of the source language and a high-level operational semantics of the target language, i.e., a subset of Haskell. We further prove that the resource consumption of an ABS program extended with a cost model is preserved over this translation, as we establish an equivalence of the cost of executing the ABS program and its corresponding Haskell-translation. Concretely, the resources consumed by the original ABS program and those consumed by the Haskell program are the same, considering a cost model. Consequently, the resource bounds automatically inferred for ABS programs extended with a cost model, using resource analysis tools, are sound resource bounds also for the translated Haskell programs. Our experimental evaluation confirms the resource preservation over a set of benchmarks featuring different asymptotic costs.

3

Operational Semantics, Interval Orders and Sequences of Antichains

Janicki Ryszard, Koutny Maciej

Fundamenta Informaticae

|

2019

|

Vol. 169, nr 1-2

31--55

EN

A representation of interval orders by sequences of antichains is discussed, and its relationship to the Fishburn’s representation by sequences of the beginnings and endings of domain elements is analysed in detail. Moreover, an operational semantics based on sequences of maximal antichains is proposed and investigated for a general class of safe Petri nets with context arcs.

4

Equational Reasoning on Mobile Ad Hoc Networks

Ghassemi F., Fokkink W., Movaghar A.

Fundamenta Informaticae

|

2011

|

Vol. 105, nr 4

375-415

EN

We provide an equational theory for Restricted Broadcast Process Theory to reason about ad hoc networks. We exploit an extended algebra called Computed Network Theory to axiomatize restricted broadcast. It allows one to define the behavior of an ad hoc network with respect to the underlying topologies. We give a sound and ground-complete axiomatization for CNT terms with finite-state behavior, modulo what we call rooted branching computed network bisimilarity.

5

Big-step Operational Semantics Revisited

Dominik J., Kuśmierek M., Bono V.

Fundamenta Informaticae

|

2010

|

Vol. 103, nr 1-4

137-172

EN

In this paper we present a novel approach to big-step operational semantics. This approach stems from the observation that the typical type soundness property formulated via a big-step operational semantics is weak, while the option of using a small-step operational semantics is not always an option, because it is less intuitive to build and understand. We support our claim by using a simple language called LM, for which we present a big-step semantics expressed with the new approach, allowing one to formulate a stronger type soundness property. We prove this property for LM and we present an example of an error in the typing rules which does not violate the typical type soundness property, but does violate ours.

6

Stochastic Petri Box Calculus with Discrete Time

Tarasyuk I.V.

Fundamenta Informaticae

|

2007

|

Vol. 76, nr 1-2

189-218

EN

In the last decades, a number of stochastic enrichments of process algebras was constructed to allow one for specification of stochastic processes within the well-developed framework of algebraic calculi. In [], a continuous time stochastic extension of finite Petri box calculus (PBC) was proposed called sPBC. The algebra sPBC has interleaving semantics due to the properties of continuous time distributions. At the same time, PBC has step semantics, and it could be natural to propose its concurrent stochastic enrichment. We construct a discrete time stochastic extension dtsPBC of finite PBC. A step operational semantics is defined in terms of labeled transition systems based on action and inaction rules. A denotational semantics is defined in terms of a subclass of labeled discrete time stochastic Petri nets (LDTSPNs) called discrete time stochastic Petri boxes (dts-boxes). A consistency of both semantics is demonstrated. In addition, we define a variety of probabilistic equivalences that allow one to identify stochastic processes with similar behaviour which are differentiated by too strict notion of the semantic equivalence. The interrelations of all the introduced equivalences are investigated.

7

A Timed Linda Language and its Denotational Semantics

de Boer F. S., Gabbrielli M., Meo M. C.

Fundamenta Informaticae

|

2004

|

Vol. 63, nr 4

309--330

EN

We introduce a Timed Linda language (T-Linda) which is obtained by a natural timed interpretation of the usual constructs of the Linda model and by adding a simple primitive which allows one to specify time-outs. Parallel execution of processes follows the scheduling policy of interleaving, however maximal parallelism is assumed for actions depending on time. We first define the operational semantics of T-Linda by means of a transition system, then we define a denotational model which is based on timed reactive sequences. The correctness of this model is proved w.r.t. a notion of observables which includes finite traces of actions and input/output pairs.

8

A formal dynamic semantics of Java: an essential ingredient of Java security

Debbabi M., Tawbi N., Yahyaoui H.

Journal of Telecommunications and Information Technology

|

2002

|

nr 4

81-120

EN

Security is becoming a major issue in our highly networked and computerized era. Malicious code detection is an essential step towards securing the execution of applications in a highly inter-connected context. In this paper, we present a formal definition of Java dynamic semantics. This semantics has been used as a basis to develop efficient, rigorous and provably correct static analysis tools and a certifying compiler aimed to detect and prevent the presence of malicious code in Java applications. We propose a small step operational semantics of a large subset for Java. The latter includes features that have not been completely addressed in the related work or addressed in another semantics style. We provide a fully-fledged semantic handling of exceptions, reachable statements, modifiers and class initialization.

9

Full abstrctness of a metric semantics for action refinement

Hartog J.I. den, Vink E.P. de, Bakker J.W. de

Fundamenta Informaticae

|

1999

|

Vol. 40, Nr 4

335-382

EN

For a process language with action refinement and synchronization both an operational and a denotational semantics are given. The operational semantics is based on an SOS-style transition system specification involving syntactical refinement sequences. The denotational semantics is an interleaving model which uses semantical refinement `environments'. It identifies those statements which are equal under all refinements. The denotational model is shown to be fully abstract with respect to the operational one. The underlying metric machinery is exploited to obtain this full abstractness result. Usually, action refinement is treated either in a model with some form of true concurrency, or, when an interleaving model is applied, by assuming that the refining statements are atomized. We argue that an interleaving model without such atomization is attractive as well.