Book
14th International Scientific-Technical Conference on Actual Problems of Electronic Instrument Engineering, APEIE 2018
In this article networks clustering methods based on a plane (space) symmetry fragmentation variants will be considered; routing in these networks based on broken symmetry groups (BSG) will be analyzed. A method for structuring a sensor network with a method clustering based on symmetry.
We establish foundational results on the computational complexity of deciding entailment in Separation Logic with general inductive predicates whose underlying base language allows for pure formulas, pointers and existentially quantified variables. We show that entailment is in general undecidable, and ExpTime-hard in a fragment recently shown to be decidable by Iosif et al. Moreover, entailment in the base language is PI_2^p complete, the upper bound even holds in the presence of list predicates. We additionally show that entailment in essentially any fragment of Separation Logic allowing for general inductive predicates is intractable even when strong syntactic restrictions are imposed.
In this article, we investigate the logical structure of memory models of theoretical and practical interest. Our main interest is in “the logic behind a fixed memory model”, rather than in “a model of any kind behind a given logical system”. As an effective language for reasoning about such memory models, we use the formalism of separation logic. Our main result is that for any concrete choice of heap-like memory model, validity in that model is undecidable even for purely propositional formulas in this language.
The main novelty of our approach to the problem is that we focus on validity in specific, concrete memory models, as opposed to validity in general classes of models.
Besides its intrinsic technical interest, this result also provides new insights into the nature of their decidable fragments. In particular, we show that, in order to obtain such decidable fragments, either the formula language must be severely restricted or the valuations of propositional variables must be constrained.
In addition, we show that a number of propositional systems that approximate separation logic are undecidable as well. In particular, this resolves the open problems of decidability for Boolean BI and Classical BI.
Moreover, we provide one of the simplest undecidable propositional systems currently known in the literature, called “Minimal Boolean BI”, by combining the purely positive implication-conjunction fragment of Boolean logic with the laws of multiplicative *-conjunction, its unit and its adjoint implication, originally provided by intuitionistic multiplicative linear logic. Each of these two components is individually decidable: the implication-conjunction fragment of Boolean logic is co-NP-complete, and intuitionistic multiplicative linear logic is NP-complete.
All of our undecidability results are obtained by means of a direct encoding of Minsky machines.
Key Words and Phrases: Separation logic, undecidability, memory models, bunched logic
We investigate the complexity consequences of adding pointer arithmetic to separation logic. Specifically, we study an extension of the points-to fragment of symbolic-heap separation logic with sets of simple “difference constraints” of the form x≤y+k
, where x and y are pointer variables and k is an integer offset. This extension can be considered a practically minimal language for separation logic with pointer arithmetic.
Most significantly, we find that, even for this minimal language, polynomial-time decidability is already impossible: satisfiability becomes NP
-complete, while quantifier-free entailment becomes coNP-complete and quantified entailment becomes ΠP2-complete (where ΠP2
is the second class in the polynomial-time hierarchy).
However, the language does satisfy the small model property, meaning that any satisfiable formula has a model, and any invalid entailment has a countermodel, of polynomial size, whereas this property fails when richer forms of arithmetical constraints are permitted.
This volume contains the papers selected for presentation at the 18th European Symposium on Research in Computer Security (ESORICS 2013), held during September 9–13, 2013, in Egham, UK. In response to the symposium’s call for papers, 242 papers were submitted to the conference from 38 countries. These papers were evaluated on the basis of their significance, novelty, technical quality, as well as on their practical impact and/or their level of advancement of the field’s foundations. The Program Committee’s work was carri ed out electronically, yielding in- tensive discussions over a period of a few weeks. Of the papers submitted, 43 were selected for presentation at the conf erence (resulting in an acceptance rate of 18%). We note that many top-quality submissions were not selected for pre- sentation because of the high technical level of the overall submissions, and we are certain that many of these submissions will, nevertheless, be published at other competitive forums in the future.
It is well-known that the Dolev–Yao adversary is a powerful adversary. Besides acting as the network, intercepting, decomposing, composing and sending messages, he can remember as much information as he needs. That is, his memory is unbounded. We recently proposed a weaker Dolev–Yao like adversary, which also acts as the network, but whose memory is bounded. We showed that this Bounded Memory Dolev–Yao adversary, when given enough memory, can carry out many existing protocol anomalies. In particular, the known anomalies arise for bounded memory protocols, where although the total number of sessions is unbounded, there are only a bounded number of concurrent sessions and the honest participants of the protocol cannot remember an unbounded number of facts or an unbounded number of nonces at a time. This led us to the question of whether it is possible to infer an upper-bound on the memory required by the Dolev–Yao adversary to carry out an anomaly from the memory restrictions of the bounded protocol. This paper answers this question negatively (Theorem 8).
In a collaborative system, the agents collaborate to achieve a common goal, but they are not willing to share some sensitive private information.
The question is how much damage can be done by a malicious participant sitting inside the system.
We assume that all the participants (including internal adversaries) have bounded memory – at any moment, they can store only a fixed number of messages of a fixed size. The Dolev–Yao adversaries can compose, decompose, eavesdrop, and intercept messages, and create fresh values (nonces), but within their bounded memory.
We prove that the secrecy problem is PSPACE-complete in the bounded memory model where all actions are balanced and a potentially infinite number of the nonce updates is allowed.
We also show that the well-known security protocol anomalies (starting from the Lowe attack to the Needham–Schroeder protocol) can be rephrased within the bounded memory paradigm with the explicit memory bounds.
This book contains the materials of the International conferencs on the problem of Economics, Engeneering and Construction.
This volume contains the proceedings of the 17th International Conference on the Foundations of Software Science and Computation Structures, FOSSACS 2014, held in Grenoble, France, 5–13 April 2014. FOSSACS is an event of the Joint European Conferences on Theory and Practice of Software (ETAPS).
FOSSACS presents original papers on the foundations of software science. The conference invited submissions on theories and methods to support analysis, synthesis, transformation, and verification of programs and software systems.
We received 128 abstracts and 106 full paper s ubmissions; of these, 28 were selected for presentation at FOSSACS and inclusion in the proceedings.
The PC members, and the external experts they consulted, wrote over 320 paper reviews, and the discussion phase of the meeting included a 3-day author rebuttal phase. The competition was very strong, and unfortunately many good papers could not be accepted.
It is well-known that the Dolev-Yao adversary is a powerful adversary. Besides acting as the network, intercepting, sending, and composing messages, he can remember as much information as he needs. That is, his memory is unbounded.
We recently proposed a weaker Dolev-Yao like adversary, which also acts as the network, but whose memory is bounded. We showed that this Bounded Memory Dolev-Yao adversary, when given enough memory, can carry out many existing protocol anomalies. In particular, the known anomalies arise for bounded memory protocols, where there is only a bounded number of concurrent sessions and the honest participants of the protocol cannot remember an unbounded number of facts nor an unbounded number of nonces at a time. This led us to the question of whether it is possible to infer an upper-bound on the memory required by the Dolev-Yao adversary to carry out an anomaly from the memory restrictions of the bounded protocol. This paper answers this question negatively (Theorem 2).
The second contribution of this paper is the formalization of Progressing Collaborative Systems that may create fresh values, such as nonces. In this setting there is no unbounded adversary, although bounded memory adversaries may be present. We prove the NP-completeness of the reachability problem for Progressing Collaborative Systems that may create fresh values.
Modern transport systems are characterized by the development and implementation of intelligent transport technologies. Today, dynamic forecast models are not used in practice in the operation of a passenger terminal. Decision making is based on some regulatory values for passenger traffic, but this is not sufficient for efficient terminal management. Modern passenger terminals are characterized by dynamic process variability and consideration of diverse options, taking into account the criteria of safety, reliability analysis, and the continuous research of passenger processing. For any modern marine passenger terminal, it is necessary to use the tool to simulate passenger flows in dynamics. Only in this way it is possible to obtain the analytical information and use it for decision making when solving the problem of the amount of personnel required for passenger service, transport safety, some forecasting tasks and so on. Of particular relevance is the choice of the mathematical transport model and the practical conditions for the implementation of the model in the real terminal operation. In this article, the analysis technique of intelligent simulation-based terminal services provides a new mathematical model of passenger movement inside the terminal and presents a new software instrument. Moreover, the conditions of implementation of some transportation models during the operation of marine passenger terminal are examined. The study represents an example of analytical information used for the forecast of the terminal operations, the analysis of the workload and the efficiency of the organization of the marine terminal.
This book constitutes the joint refereed proceedings of the 17th International Conference on Next Generation Wired/Wireless Advanced Networks and Systems, NEW2AN 2017, the 10th Conference on Internet of Things and Smart Spaces, ruSMART 2017. The 71 revised full papers presented were carefully reviewed and selected from 202 submissions. The papers of NEW2AN focus on advanced wireless networking and applications; lower-layer communication enablers; novel and innovative approaches to performance and efficiency analysis of ad-hoc and machine-type systems; employed game-theoretical formulations, Markov chain models, and advanced queuing theory; grapheme and other emerging material, photonics and optics; generation and processing of signals; and business aspects. The ruSMART papers deal with fully-customized applications and services. The NsCC Workshop papers capture the current state-of-the-art in the field of molecular and nanoscale communications such as information, communication and network theoretical analysis of molecular and nanonetwork, mobility in molecular and nanonetworks; novel and practical communication protocols; routing schemes and architectures; design/engineering/evaluation of molecular and nonoscale communication systems; potential applications and interconnections to the Internet (e.g. the Internet of Nano Things).
14th International Scientific-Technical Conference on Actual Problems of Electronics Instrument Engineering, APEIE 2018 - Proceedings
Описывается созданный макет манипулятора с биоэлектрическим управлением. Манипулятор сделан в форме человеческой ладони, движение пальцев которой управляется через электромиосигналы оператора. В среде LabVIEW разработан виртуальный прибор, позволяющий с помощью дискретного вейвлет-преобразования осуществить анализ электромиосигналов оператора, определить моменты мышечной активности и сформировать по результатам анализа сигналы управления манипулятором.
Let G be a semisimple algebraic group whose decomposition into the product of simple components does not contain simple groups of type A, and P⊆G be a parabolic subgroup. Extending the results of Popov [7], we enumerate all triples (G, P, n) such that (a) there exists an open G-orbit on the multiple flag variety G/P × G/P × . . . × G/P (n factors), (b) the number of G-orbits on the multiple flag variety is finite.
I give the explicit formula for the (set-theoretical) system of Resultants of m+1 homogeneous polynomials in n+1 variables