Wyniki wyszukiwania - BazTech

1

A Function Elimination Method for Checking Satisfiability of Arithmetical Logics

Castiglioni V., Lanotte R., Tini S.

Fundamenta Informaticae

|

2016

|

Vol. 143, nr 1/2

51--71

EN

We study function elimination for Arithmetical Logics. We propose a method allowing substitution of functions occurring in a given formula with functions with less arity. We prove the correctness of the method and we use it to show the decidability of the satisfiability problem for two classes of formulas allowing linear and polynomial terms.

2

A Specification Format for Rooted Branching Bisimulation

Castiglioni V., Lanotte R., Tini S.

Fundamenta Informaticae

|

2014

|

Vol. 135, nr 4

355--369

EN

Rule formats are sets of syntactical constraints over SOS rules ensuring semantical properties of the derived LTS. Given a rule format, our proposal is to relax the constraints imposed on each single rule and to introduce some constraints on the form of the whole set of rules, thus obtaining a new format ensuring the same semantical property and being less demanding than the original one. We apply our idea to a well known rule format for rooted branching bisimulation equivalence.

3

A Decidable Probability Logic for Timed Probabilistic Systems

Lanotte R., Beauquier D.

Fundamenta Informaticae

|

2009

|

Vol. 96, nr 1/2

127-151

EN

In this paper we extend the predicate logic introduced by Beauquier et al. in order to deal with Markov decision processes. We prove that with respect to qualitative probabilistic properties, model checking is decidable for this logic applied to Markov decision processes. Furthermore we apply our logic to probabilistic timed transition systems using predicates on clocks. We prove that results on Markov decision processes hold also for probabilistic timed transition systems. The interest of this logic lies in particular on the fact that some important properties are expressible in this logic but not expressible in pCTL.

4

Dynamic Hierarchical Machines

Lanotte R., Maggiolo-Schettini A., Peron A., Tini S.

Fundamenta Informaticae

|

2003

|

Vol. 54, nr 2,3

237-252

EN

We present Dynamic Hierarchical Machines (DHMs), an extension of Communicating Hierarchical Automata allowing dynamic activation of components. We give an operational semantics of DHMs and we provide examples of modeling in the context of security. We characterize a fragment of DHMs which are equivalent to Recursive Hierarchical Machines and therefore to Pushdown Machines.

5

Transformations of Timed Cooperating Automata

Lanotte R., Maggiolo-Schettini A., Tini S., Peron A.

Fundamenta Informaticae

|

2001

|

Vol. 47, nr 3,4

271-282

EN

The paper pursues the investigation of Timed Cooperating Automata (TCAs) by studying transformations which are suggested as means for stepwise TCA construction.

6

Timed Cooperating Automata

Lanotte R., Maggiolo-Schettini A.

Fundamenta Informaticae

|

2000

|

Vol. 43, Nr 1-4

153-173

EN

We propose Timed Cooperating Automata (TC As), an extension of the model Cooperating Automata of Harel and Drusinsky, and we investigate some basic properties. In particular we consider variants of TCAs based on the presence or absence of internal activity, urgency and reactivity, and we compare the expressiveness of these variants with that of the classical model of Timed Automata (TAs) and its extensions with periodic clock constraints and with silent moves. We consider also closure and decidability properties of TCAs and start a study on succinctness of their variants with respect to that of TAs.