Wyniki wyszukiwania - BazTech

1

A Representation Theorem for Primitive Recursive Algorithms

Andary P., Patrou B., Valarcher P.

Fundamenta Informaticae

|

2011

|

Vol. 107, nr 4

313-330

EN

We formalize the algorithms computing primitive recursive (PR) functions as the abstract state machines (ASMs) whose running length is computable by a PR function. Then we show that there exists a programming language (implementing only PR functions) by which it is possible to implement any one of the previously defined algorithms for the PR functions in such a way that their complexity is preserved.

2

Time in State Machines

Graf S., Prinz A.

Fundamenta Informaticae

|

2007

|

Vol. 77, nr 1,2

143-174

EN

State machines are a very general means to express computations in an implementation-independent way. There are ways to extend the abstract state machine (ASM) framework with distribution aspects, but there is no unifying framework for handling time so far. We propose event structures extended with time as a natural framework for representing state machines and their true concurrency model at a semantic level and for discussing associated time models. Constraints on these timed event structures and their traces (runs) are then used for characterising different frameworks for timed computations. This characterisation of timed frameworks is independent of ASM and allows to compare time models of different modelling formalisms. Finally, we propose some specific extensions of ASM for the expressions of time constraints in accordance with the event-based semantic framework and show the applicability of the obtained framework on an example with a standard time model and a set of consistency properties for timed computations.

3

RAM Simulation of BGS Model of Abstract-state Machines

Seshadhri S., Seth A., Biswas S.

Fundamenta Informaticae

|

2007

|

Vol. 77, nr 1,2

175-185

EN

We show in this paper that the BGS model of abstract state machines can be simulated by random access machines with at most a polynomial time overhead. This result is already stated in [5] with a very brief proof sketch. The present paper gives a detailed proof of the result. We represent hereditarily finite sets, which are the typical BGS ASM objects, by membership graphs of the transitive closure of the sets. Testing for equality between BGS objects can be done in linear time in our representation.

4

Model Checking Abstract State Machines with Answer Set Programming

Tang C.K.F., Ternovska E.

Fundamenta Informaticae

|

2007

|

Vol. 77, nr 1,2

105-141

EN

The quality of a computer system can be enhanced by modelling its design and verifying the correctness of the design before implementation is done. Abstract State Machines (ASMs) provide a mathematical framework for system modelling, while Model Checking is a technology for verification of system properties. Together, they form a powerful tool for checking systems. Bounded Model Checking (BMC) based on Answer Set Programming (ASP) is a competitive model checking approach due to its ability to compactly encode BMC problems. In this paper, we present a method of applying ASP to BMC of ASMs. Given an ASM and a temporal property, we show how to efficiently translate the BMC problem for the ASM into a problem of answer set computation. Experimental results for our method using the answer set solvers SMODELS and CMODELS are also given.

5

CoreASM: An Extensible ASM Execution Engine

Farahbod R., Gervasi V., Glässer U.

Fundamenta Informaticae

|

2007

|

Vol. 77, nr 1,2

71-103

EN

In this paper we introduce a new research effort in making abstract state machines (ASMs) executable. The aim is to specify and implement an execution engine for a language that is as close as possible to the mathematical definition of pure ASMs. The paper presents the general architecture of the engine, together with a high-level description of the extensibility mechanisms that are used by the engine to accommodate arbitrary backgrounds, scheduling policies, and new rule forms.