Wyniki wyszukiwania - BazTech

1

The possibility of use of mixture of siliceous and calcareous fly ash for production of Portland-composite cement type CEM II/B-M (V-W) 52.5

Tkaczewska Ewelina

Roads and Bridges - Drogi i Mosty

|

2020

|

Vol. 19, no. 4

267--282

EN

The paper analyses the properties of Portland-composite cement CEM II/B-M (V-W) prepared by addition of mixture of siliceous and calcareous fly ashes – in percentage proportion of 20:0, 10:10, 20:10 or 15:15 – to Portland cement CEM I 42.5R. Blaine’s surface area of cements equalled 4000±100 cm2/g. Hydration heat, standard consistency, initial setting time, soundness and compressive strength were analysed in the paper. Partial replacement of siliceous fly ash with calcareous fly ash in cement gives a Portland-composite cement CEM II/B-M (V-W) of strength class 52.5N or even 52.5R, if the percentage proportion of siliceous to calcareous fly ash is 20:10.

PL

Przedmiotem artykułu jest analiza właściwości cementu portlandzkiego wieloskładnikowego CEM II/B-M (V-W) otrzymanego przez dodanie do cementu portlandzkiego CEM I 42,5R mieszaniny popiołów lotnych – krzemionkowego i wapiennego – zmieszanych w proporcji 20:0, 10:10, 20:10 lub 15:15. Powierzchnia właściwa badanych cementów według metody Blaine'a wynosiła 4000±100 cm2/g. W artykule przeprowadzono analizę ciepła hydratacji, konsystencji normowej, początku czasu wiązania, stałości objętości i wytrzymałości na ściskanie. Częściowe zastąpienie popiołu krzemionkowego popiołem wapiennym w cemencie wieloskładnikowym CEM II/B-M (V-W) pozwoliło uzyskać cement o klasie wytrzymałości 52,5N lub nawet 52,5R w przypadku zmieszania popiołu krzemionkowego i wapiennego w proporcji 20:10.

2

A Propositional Metric Logic with Fixed Finite Ranges

Djordjević Radosav, Ikodinović Nebojša, Stojanović Nenad

Fundamenta Informaticae

|

2020

|

Vol. 174, nr 2

185--199

EN

The aim of this article is developing a formal system suitable for reasoning about the distance between propositional formulas. We introduce and study a formal language which is the extension of the classical propositional language obtained by adding new binary operators D≤s and D≥s , s ∈ Range, where Range is a fixed finite set. In our language it is allowed to make formulas of the form D≤s (α ; β ) with the intended meaning ’distance between formulas α and β is less than or equal to s ’. The semantics of the proposed language consists of possible worlds with a distance function defined between sets of worlds.

3

The influence of cement bypass dust on the properties of cement curing under normal and autoclave conditions

Tkaczewska Ewelina

Structure and Environment

|

2019

|

Vol. 11, no. 1

5--22

EN

This paper analyses the properties of cement binders composed with cement CEM I 42.5R and cement bypass dust in amount of 0.5, 1.0 and 5.0% by mass of binder, curing under standard and additionally autoclave conditions. The bypass dust increases the water content for standard consistency and delays the initial setting time of binder. The cement paste containing 5% of dust reveals the change in volume by 6 mm according to Le Chatelier test. After 2 days, the compressive strength of cement mortar containing bypass is comparable to that of Portland cement mortar, but at later time the strength development of this cement binder is slower. The addition of cement bypass dust in amount to 1% can obtain the cement of strength class of 42.5R according to standard PN-EN 197-1. The autoclave curing improves the compressive strength of cement mortar. The SEM/EDS observations confirm the presence of low crystalline C-S-H gel and well-formed tobermorite fibres in autoclaved cement mortar containing 5% of cement bypass dust.

PL

W pracy analizowano właściwości spoiw cementowych zawierających w składzie cement portlandzki CEM I 42,5R i pył z instalacji bypassa pieca cementowego w ilości 0,5, 1,0 i 5,0% masy spoiwa, dojrzewających w warunkach normalnych i dodatkowo w autoklawie. Pył z bypassa zwiększa ilość wody niezbędnej do uzyskania konsystencji normowej oraz opóźnia początek czasu wiązania spoiwa. Zaczyn zawierający 5% pyłu wykazuje zmianę objętości o 6 mm według Le Chateliera. Po dwóch dniach wytrzymałość na ściskanie zaprawy ze spoiwa zawierającego pył z bypassa jest porównywalna z wytrzymałością zaprawy z cementu portlandzkiego, ale w miarę upływu czasu przyrost wytrzymałości zaprawy z tego spoiwa jest mniejszy. Dodatek pyłu z bypassa w ilości nieprzekraczającej 1% pozwala otrzymać cement klasy wytrzymałości 42,5R według wymagań normy PN-EN 197-1. Autoklawizacja zwiększa wytrzymałość na ściskanie zaprawy cementowej, a pył z bypassa stanowi jeden z czynników poprawiających właściwości wytrzymałościowe. Obserwacje SEM/EDS potwierdzają obecność słabo wykrystalizowanego żelu C-S-H i dobrze wykształconych włókien tobermorytu w próbce zaprawy zawierającej 5% pył z bypassa dojrzewającej w warunkach autoklawu.

4

The Duality of Classical Intersection and Union Types

Downen Paul, Ariola Zena M., Ghilezan Silvia

Fundamenta Informaticae

|

2019

|

Vol. 170, nr 1-3

39--92

EN

For a long time, intersection types have been admired for their surprising ability to complete the simply typed lambda calculus. Intersection types are an example of an implicit typing feature which can describe program behavior without manifesting itself within the syntax of a program. Dual to intersections, union types are another implicit typing feature which extends the completeness property of intersection types in the lambda calculus to full-fledged programming languages. However, the formalization of union types can easily break other desirable meta-theoretical properties of the type system. But why should unions be troublesome when their dual, intersections, are not? We look at the issues surrounding the design of type systems for both intersection and union types through the lens of duality by formalizing them within the symmetric language of the classical sequent calculus. In order to formulate type systems which have all of our properties of interest—soundness, completeness, and type safety—we also look at the impact of evaluation strategy on typing. As a result, we present two dual type systems—one for call-by-value and one for call-by-name evaluation—which have all three properties. We also consider the possibility of classical non-deterministic evaluation, for which there is a choice between two different systems depending on which properties are desired: a full type system which is complete, and a simplified type system which is sound and type safe.

5

On Generating Hierarchical Workflow Nets and their Extensions and Verifying Hierarchicality

Sroka J., Chrząstowski-Wachtel P., Hidders J.

Fundamenta Informaticae

|

2015

|

Vol. 141, nr 4

367--398

EN

For designing and analyzing complex workflow nets the notion of hierarchical decomposition can be essential for keeping the structure of the workflow comprehensible. In this paper we study two classes of nets: hierarchical nets and extended hierarchical nets. The first have a simple hierarchical structure and can be defined in terms of five simple refinement rules. We show that for arbitrary nets it can be easily verified if they can be constructed this way, thus confirming their good design and the properties following from it. As we prove, this can be done by performing the refinements in reverse, i.e., by contracting subnets into single nodes. It is shown that the choice of the contracted subnet does not change the final result of the process, and therefore this procedure for checking the hierarchical structure requires no back-tracking. The second class, extended hierarchical nets, is an extension of the first class where two types of extra refinements are introduced that allow to indicate (1) the synchronization between two parallel running subworkflows or (2) the transfer of a thread from one subworkflow to another one. These refinements come with natural and necessary preconditions that ensure that result is still a sound workflow net. In case (1) where we want to synchronize two actions in two subworkflows, we should convince ourselves that the subworkflows represent parallel threads which always execute together, otherwise a deadlock could easily arise. Dually, in case (2), if after the moment that a choice was made between two subworkflows we at a later point in the workflow want to allow a transfer between them, this can be done safely provided that we did not enter any thread fork in the meantime. We show that the class of extended hierarchical nets, which is defined by adding these two additional types of refinement, is a proper superset of the hierarchical nets, but still all such nets exhibit the correctness property of *-soundness. We do this by showing that the class is a proper subset of the AND-OR nets which were in earlier work shown to have this property.

6

An analytical method for well-formed workflow/Petri net verification of classical soundness

Clempner J.

International Journal of Applied Mathematics and Computer Science

|

2014

|

Vol. 24, no. 4

931--939

EN

In this paper we consider workflow nets as dynamical systems governed by ordinary difference equations described by a particular class of Petri nets. Workflow nets are a formal model of business processes. Well-formed business processes correspond to sound workflow nets. Even if it seems necessary to require the soundness of workflow nets, there exist business processes with conditional behavior that will not necessarily satisfy the soundness property. In this sense, we propose an analytical method for showing that a workflow net satisfies the classical soundness property using a Petri net. To present our statement, we use Lyapunov stability theory to tackle the classical soundness verification problem for a class of dynamical systems described by Petri nets. This class of Petri nets allows a dynamical model representation that can be expressed in terms of difference equations. As a result, by applying Lyapunov theory, the classical soundness property for workflow nets is solved proving that the Petri net representation is stable. We show that a finite and non-blocking workflow net satisfies the sound property if and only if its corresponding PN is stable, i.e., given the incidence matrix A of the corresponding PN, there exists a Φ strictly positive m vector such that AΦ ≤ 0. The key contribution of the paper is the analytical method itself that satisfies part of the definition of the classical soundness requirements. The method is designed for practical applications, guarantees that anomalies can be detected without domain knowledge, and can be easily implemented into existing commercial systems that do not support the verification of workflows. The validity of the proposed method is successfully demonstrated by application examples.

7

Complexity of the Soundness Problem of Workflow Nets

Liu G. J., Sun J., Liu Y., Dong J. S.

Fundamenta Informaticae

|

2014

|

Vol. 131, nr 1

81--101

EN

Classical workflow nets (WF-nets for short) are an important subclass of Petri nets that are widely used to model and analyze workflow systems. Soundness is a crucial property of workflow systems and guarantees that these systems are deadlock-free and bounded. Aalst et al. proved that the soundness problem is decidable for WF-nets and can be polynomially solvable for free-choice WF-nets. This paper proves that the soundness problem is PSPACE-hard for WF-nets. Furthermore, it is proven that the soundness problem is PSPACE-complete for bounded WF-nets. Based on the above conclusion, it is derived that the soundness problem is also PSPACE-complete for bounded WF-nets with reset or inhibitor arcs (ReWF-nets and InWF-nets for short, resp.). ReWF- and InWF-nets are two extensions to WF-nets and their soundness problems were proven by Aalst et al. to be undecidable. Additionally, we prove that the soundness problem is co-NP-hard for asymmetric-choice WF-nets that are a larger class and can model more cases of interaction and resource allocation than free-choice ones.

8

Apriori-Based Rule Generation in Incomplete Information Databases and Non-Deterministic Information Systems

Sakai H., Wu M., Nakata M.

Fundamenta Informaticae

|

2014

|

Vol. 130, nr 3

343--376

EN

This paper discusses issues related to incomplete information databases and considers a logical framework for rule generation. In our approach, a rule is an implication satisfying specified constraints. The term incomplete information databases covers many types of inexact data, such as non-deterministic information, data with missing values, incomplete information or interval valued data. In the paper, we start by defining certain and possible rules based on non-deterministic information. We use their mathematical properties to solve computational problems related to rule generation. Then, we reconsider the NIS-Apriori algorithm which generates a given implication if and only if it is either a certain rule or a possible rule satisfying the constraints. In this sense, NIS-Apriori is logically sound and complete. In this paper, we pay a special attention to soundness and completeness of the considered algorithmic framework, which is not necessarily obvious when switching from exact to inexact data sets. Moreover, we analyze different types of non-deterministic information corresponding to different types of the underlying attributes, i.e., value sets for qualitative attributes and intervals for quantitative attributes, and we discuss various approaches to construction of descriptors related to particular attributes within the rules' premises. An improved implementation of NIS-Apriori and some demonstrations of an experimental application of our approach to data sets taken from the UCI machine learning repository are also presented. Last but not least, we show simplified proofs of some of our theoretical results.

9

Interacting Workflow Nets for Workflow Process Re-Engineering

Lomazova I.A.

Fundamenta Informaticae

|

2010

|

Vol. 101, nr 1/2

59-70

EN

In this work we consider modeling of workflow systems with Petri nets. To increase flexibility and give tools for workflow models re-engineering we extend the formalism of workflow nets by considering systems of interacting nets. Then we study soundness – the main correctness property of workflow processes – and show, that for a special class of structured workflow system soundness can be proved in compositional way.

10

Checking Properties of Adaptive Workflow Nets

van Hee K., Oanea O., Serebrenik A., Sidorova N., Voorhoeve M., Lomazova I.A.

Fundamenta Informaticae

|

2007

|

Vol. 79, nr 3-4

347-362

EN

In this paper we consider adaptive workflow nets, a class of nested nets that allows more comfort and expressive power for modeling adaptability and exception handling in workflow nets. We define two important behavioural properties of adaptive workflow nets: soundness and circumspectness. Soundness means that a proper final marking (state) can be reached from any marking which is reachable from the initial marking, and no garbage will be left. Circumspectness means that the upper layer is always ready to handle any exception that can happen in a lower layer. We define a finite state abstraction for adaptive workflow nets and show that soundness and circumspectness can be verified on this abstraction.