Wyniki wyszukiwania - BazTech

1

Semantics for Specialising Attack Trees based on Linear Logic

Horne R., Mauw S., Tiu A.

Fundamenta Informaticae

|

2017

|

Vol. 153, nr 1/2

57--86

EN

Attack trees profile the sub-goals of the proponent of an attack. Attack trees have a variety of semantics depending on the kind of question posed about the attack, where questions are captured by an attribute domain. We observe that one of the most general semantics for attack trees, the multiset semantics, coincides with a semantics expressed using linear logic propositions. The semantics can be used to compare attack trees to determine whether one attack tree is a specialisation of another attack tree. Building on these observations, we propose two new semantics for an extension of attack trees named causal attack trees. Such attack trees are extended with an operator capturing the causal order of sub-goals in an attack. These two semantics extend the multiset semantics to sets of series-parallel graphs closed under certain graph homomorphisms, where each semantics respects a class of attribute domains. We define a sound logical system with respect to each of these semantics, by using a recently introduced extension of linear logic, called MAV, featuring a non-commutative operator. The non-commutative operator models causal dependencies in causal attack trees. Similarly to linear logic for attack trees, implication defines a decidable preorder for specialising causal attack trees that soundly respects a class of attribute domains.

2

Between syntax and semantics of resource oriented logic for ids behavior description

Perhac J., Mihalyi D., Novitzka V.

Journal of Applied Mathematics and Computational Mechanics

|

2016

|

Vol. 15, nr 2

105--118

EN

Linear logic appears as a suitable logical system for description of dynamic properties of various network activities in computer science. It disposes with new connectives which create new opportunities to describe properties of real network processes, e.g. parallelism, causality and commutativity of duality between processes. We extend this logic with Aristotelian modalities and we formulate their appropriate model. In our contribution we show how a real network attack can be formalized in this logical system as a polarized game.

3

Linear logic in computer science

Steingartner W., Poláková A., Prazňák P., Novitzká V.

Journal of Applied Mathematics and Computational Mechanics

|

2015

|

Vol. 14, nr 1

91--100

EN

Linear logic has many properties that make it suitable for application in various areas of computer science. It is able to describe dynamic processes, non-determinism, parallelism on syntactic level. In our paper we try to discuss resource oriented character of linear logic, its possibility to deal with such important resources for computer science as space (memory) and time. Handling with resources takes place in deduction system of linear logic. We show how special form of proofs, called designs, is constructed and we show the relationship between space and time in designs.

4

Negation as a Resource: a Novel View on Answer Set Semantics

Costantini S., Formisano A.

Fundamenta Informaticae

|

2015

|

Vol. 140, nr 3/4

279--305

EN

In recent work, we provided a formulation of ASP programs in terms of linear logic theories. Answer sets were characterized in terms of maximal tensor conjunctions provable from such theories. In this paper, we propose a full comparison between Answer Set Semantics and its variation obtained by interpreting literals (including negative literals) as resources, which leads to a different interpretation of negation. We argue that this novel view can be of both theoretical and practical interest, and we propose a modified Answer Set Semantics that we call Resource-based Answer Set Semantics. An advantage is that of avoiding inconsistencies, as every program has a (possibly empty) resource-based answer set. This implies however the introduction of a different way of representing constraints. We provide a characterization of the new semantics as a variation of the answer set semantics, and also in terms of Autoepistemic Logic. The latter characterization leads to a way of computing resource-based answer set via answer set solvers.

5

Reasoning about resources and information : a linear logic approach

Kamide N., Kaneiwa K.

Fundamenta Informaticae

|

2013

|

Vol. 125, nr 1

51--70

EN

A logic called sequence-indexed linear logic (SLL) is proposed to appropriately formalize resource-sensitive reasoning with sequential information. The completeness and cut-elimination theorems for SLL are proved, and SLL and a fragment of SLL are shown to be undecidable and decidable, respectively. As an application of SLL, some specifications of secure password authentication systems are discussed.

6

About Parallel and Syntactocentric Formalisms: A Perspective from the Encoding of Convergent Grammar into Abstract Categorial Grammar

Groote P., de, Pogodalla S., Pollard C.

Fundamenta Informaticae

|

2011

|

Vol. 106, nr 2-4

211-231

EN

Recent discussions of grammatical architectures have distinguished two competing approaches to the syntax-semantics interface: syntactocentrism, wherein syntactic structures are mapped or transduced to semantics (and phonology), vs. parallelism, wherein semantics (and phonology) communicates with syntax via a nondirectional (or relational) interface. This contrast arises for instance in dealing with in situ operators. The aim of this paper is threefold: first, we show how the essential content of a parallel framework, convergent grammar (CVG), can be encoded within abstract categorial grammar (ACG), a generic framework which has mainly been used, until now, to encode syntactocentric architectures. Second, using such a generic framework allows us to relate the mathematical characterization of parallelism in CVG with that of syntactocentrism in mainstream categorial grammar (CG), suggesting that the distinction between parallel and syntactocentric formalisms is superficial in nature. More generally, it shows how to provide mildly context sensitive languages (MCSL), which are a clearly defined class of languages in terms of ACG, with a relational syntax-semantics interface. Finally, while most of the studies on the generative power of ACG have been related to formal languages, we show that ACG can illuminate a linguistically motivated framework such as CVG.

7

A Study of Interconnections Between Rough and 3-Valued Łukasiewicz Logics

Sen J., Chakraborty M.K.

Fundamenta Informaticae

|

2002

|

Vol. 51, nr 3

311-324

EN

Sequent calculi for topological quasi-Boolean algebras, topological quasi-Boolean algebras without distributivity, pre-rough algebras and Wajsberg algebras have been presented. It is shown that the calculi for the latter two classes of algebras are equivalent. A connection between some logics for the first class of algebras and the linear logic or linear logic with distributivity has been established.

8

A Multi-region Linear Logic based calculus for dynamic Petri net structures

Farwer B.

Fundamenta Informaticae

|

2000

|

Vol. 43, Nr 1-4

61-79

EN

Object based Petri nets are becoming increasingly popular in many fields of computer science. The possibility to model real-world objects as separate Petri nets supports the need for modular design of complex systems. So far object net approaches have been based on the presumption that the object nets' structure remains unchanged in all processes. This paper sheds some light on possible extensions of high-level Petri nets to incorpo-rate the dynamical evolution of Petri net structures. The exposition is based on the Linear Logic encoding of Petri nets, and coloured Petri nets. It provides a basic se-mantics for modifying net structures which can be employed in a framework of nets within nets, i.e. situations where Petri nets (so-called token nets) themselves are used as tokens in an underlying environment net.

9

A Linear Logic view of object Petri Nets

Farwer B.

Fundamenta Informaticae

|

1999

|

Vol. 37, Nr 3

225-246

EN

Linear Logic has been shown to incorporate a fragment suitable for representing P/T-nets and giving a semantics to the computations of such nets. This result is generalized to coloured nets. Furthermore a new kind of high-level nets is defined: Linear Logic Petri Nets (LLPN). These nets are used as an intuitive semantics to well-known and new high-level net concepts like object systems and agent orientation.