Modal context restriction for multiagent BDI logics

We present and discuss a novel language restriction for modal logics for multiagent systems, called modal context restriction, that reduces the complexity of the satisfiability problem from EXPTIME complete to NPTIME complete. We focus on BDI multimodal logics that contain fix-point modalities like common beliefs and mutual intentions together with realism and introspection axioms. We show how this combination of modalities and axioms affects complexity of the satisfiability problem and how it can be reduced by restricting the modal context of formulas.

Double Kodaira fibrations with small signature

Kodaira fibrations are surfaces of general type with a non-isotrivial fibration, which are differentiable fiber bundles. They are known to have positive signature divisible by [Formula: see text]. Examples are known only with signature 16 and more. We review approaches to construct examples of low signature which admit two independent fibrations. Special attention is paid to ramified covers of product of curves which we analyze by studying the monodromy action for bundles of punctured curves. As a by-product, we obtain a classification of all fix-point-free automorphisms on curves of genus at most [Formula: see text].

Platform-independent Specification and Verification of the Standard Mathematical Square Root Function

The project “Platform-independent approach to formal specification and verification of standard mathematical functions” is aimed onto the development of incremental combined approach to specification and verification of standard Mathematical functions like sqrt, cos, sin, etc. Platform-independence means that we attempt to design a relatively simple axiomatization of the computer arithmetics in terms of real arithmetics (i.e. the field \(\mathbb{R}\) of real numbers) but do not specify neither base of the computer arithmetics, nor a format of numbers representation. Incrementality means that we start with the most straightforward specification of the simplest case to verify the algorithm in real numbers and finish with a realistic specification and a verification of the algorithm in computer arithmetics. We call our approach combined because we start with manual (pen-and-paper) verification of the algorithm in real numbers, then use this verification as proof-outlines for a manual verification of the algorithm in computer arithmetics, and finish with a computer-aided validation of the manual proofs with a proof-assistant system (to avoid appeals to “obviousness” that are common in human-carried proofs). In the paper, we apply our platform-independent incremental combined approach to specification and verification of the standard Mathematical square root function. Currently a computer-aided validation was carried for correctness (consistency) of our fix-point arithmetics and for the existence of a look-up table with the initial approximations of the square roots for fix-point numbers.

Loopfrog — loop summarization for static analysis

Loopfrog is a scalable static analyzer for ANSI-C programs, that combines the precision of model checking and the performance of abstract interpretation. In contrast to traditional static analyzers, it does not calculate the abstract fix-point of a program by iterative application of an abstract transformer. Instead, it calculates symbolic abstract transformers for program fragments (e.g., loops) using a loop summarization algorithm. Loopfrog computes abstract transformers starting from the inner-most loops, which results in linear (in the number of the looping constructs) run-time of the sum- marization procedure and which is often considerably smaller than the traditional saturation procedure of abstract interpetation. It also provides “leaping” counterexamples to aid in the diagnosis of errors.

Coexisting Oscillation and Extreme Multistability for a Memcapacitor-Based Circuit

The coexisting oscillations are observed with a memcapacitor-based circuit that consists of two linear inductors, two linear resistors, and an active nonlinear charge-controlled memcapacitor. We analyze the dynamics of this circuit and find that it owns an infinite number of equilibrium points and coexisting attractors, which means extreme multistability arises. Furthermore, we also show the stability of the infinite many equilibria and analyze the coexistence of fix point, limit cycle, and chaotic attractor in detail. Finally, an experimental result of the proposed oscillator via an analog electronic circuit is given.