Wyniki wyszukiwania - BazTech

1

State Complexity of Multiple Catenations

Caron P., Luque J.-G., Patrou B.

Fundamenta Informaticae

|

2018

|

Vol. 160, nr 3

255--279

EN

We improve some results relative to the state complexity of the multiple catenations described by Gao and Yu. In particular we nearly divide by 2 the size of the alphabet needed for witnesses. We also give some refinements to the algebraic expression of the state complexity, which is especially complex with this operation. We obtain these results by using peculiar DFAs defined by Brzozowski.

2

SMT-Based Reachability Checking for Bounded Time Petri Nets

Półrola A., Cybula P., Męski A.

Fundamenta Informaticae

|

2014

|

Vol. 135, nr 4

467--482

EN

Time Petri nets by Merlin and Farber are a powerful modelling formalism. However, symbolic model checking methods for them consider in most cases the nets which are 1-safe, i.e., allow the places to contain at most one token. In our paper we present an approach which applies symbolic verification to testing reachability for time Petri nets without this restriction. We deal with the class of bounded nets restricted to disallow multiple enabledness of transitions, and present the method of reachability testing based on a translation into a satisfiability modulo theory (SMT).

3

Constant-Space P Systems with Active Membranes

Leporati A., Manzoni L., Mauri G., Porreca A. E., Zandron C.

Fundamenta Informaticae

|

2014

|

Vol. 134, nr 1/2

111--128

EN

We show that a constant amount of space is sufficient to simulate a polynomial-space bounded Turing machine by P systems with active membranes. We thus obtain a new characterisation of PSPACE, which raises interesting questions about the definition of space complexity for P systems. We then propose an alternative definition, where the size of the alphabet and the number of membrane labels of each P system are also taken into account. Finally we prove that, when less than a logarithmic number of membrane labels is available, moving the input objects around the membrane structure without rewriting them is not enough to even distinguish inputs of the same length.

4

Checking MTL Properties of Discrete Timed Automata via Bounded Model Checking

Woźna-Szcześniak B., Zbrzezny A.

Fundamenta Informaticae

|

2014

|

Vol. 135, nr 4

553--568

EN

We investigate a SAT-based bounded model checking (BMC) method for MTL (metric temporal logic) that is interpreted over linear discrete infinite time models generated by discrete timed automata. In particular, we translate the existential model checking problem for MTL to the existential model checking problem for a variant of linear temporal logic (called HLTL), and we provide a SAT-based BMC technique for HLTL. We show how to implement the BMC technique for HLTL and discrete timed automata, and as a case study we apply the technique in the analysis of GTPP, a Generic Timed Pipeline Paradigm modelled by a network of discrete timed automata.

5

Uniform bounds for Bessel functions

Krasikov I.

Journal of Applied Analysis

|

2006

|

Vol. 12, nr 1

83-91

EN

For ν > -1/2 and x real we shall establish explicit bounds for the Bessel function Jν(x) which are uniform in x and ν. This work and the recent result of L. J. Landau [7] provide sharp inequalities for all real x.

6

Bounds for the effective shear modulus

Ecsedi I.

Engineering Transactions

|

2005

|

Vol. 53, iss. 4

415-423

EN

This paper deals with the uniform torsion of nonhomogeneus elastic beams. The concept of the effective shear modulus is deduced from torsional rigidity. Upper and lower bounds are derived for the effective shear modulus. It is proven that the effective shear modulus of a~compound beam is between the weighted arithmetic and harmonic means of shear moduli of the beam components.

7

Difference between weighted integral means

Cerone P.

Demonstratio Mathematica

|

2002

|

Vol. 35, nr 2

251-265

EN

Weighted integral means over [c, d] and [a, b] where [c, d] C [a, 6] are compared in the current work by determining bounds for their difference in terms of a variety of norms. The bounds are obtained and involve the behaviour of at most the first derivative. Previous work for unweighted integral means is recaptured as particular cases if the weights are taken to be unity. By a limiting shrinking of the subinterval [c, d] to a single point, weighted Ostrowski type inequalities are shown to be recaptured, under certain conditions as particular instances of the current development.