Search

Sometimes Artificial Intelligence (AI) has to deal with undecided problems. An undecided problem has no computer solution. The non-monotonic problem is undecided. Fuzzy logic will make undecided into decided. Fuzzy logic with twofold fuzzy set will give conclusion for non-monotonic reasoning. In this paper, Fuzzy non-monotonic reasoning is studied with twofold fold fuzzy membership functions belief and disbelief twofold to made undecided problem in to decidable. Fuzzy certainty factor (FCF) is defined to eliminate conflict between belief and disbelief. Fuzzy truth maintenance system (FTMS) is studied for computation of fuzzy non-monotonic reasoning to make monotonic. Some examples are given for fuzzy non-monotonic reasoning.

We establish decidability for the infinitely many axiomatic extensions of the commutative Full Lambek logic with weakening FLew (i.e. IMALLW) that have a cut-free hypersequent proof calculus (specifically: every analytic structural rule extension). Decidability for the corresponding extensions of its contraction counterpart FLec was established recently but their computational complexity was left unanswered. In the second part of this paper, we introduce just enough on length functions for well-quasi-orderings and the fast-growing complexity classes to obtain complexity upper bounds for both the weakening and contraction extensions. A specific instance of this result yields the first complexity bound for the prominent fuzzy logic MTL (monoidal t-norm based logic) providing an answer to a long-standing open problem., Comment: Accepted for publication in the proceedings of LICS 2021

International audience; Using a combination of automata-theoretic and game-semantic techniques, we propose a method for analysing higher-order concurrent programs. Our language of choice is Finitary Idealised Concurrent Algol (FICA) due to its relatively simple fully abstract game model. Our first contribution is an automata model over a treestructured infinite data alphabet, called split automata, whose distinctive feature is the separation of control and memory. We show that every FICA term can be translated into such an automaton. Thanks to the structure of split automata, we are able to observe subtle aspects of the underlying game semantics. This enables us to identify a fragment of FICA with iteration and limited synchronisation (but without recursion), for which, in contrast to the whole FICA, a variety of verification problems turn out to be decidable.

The notion of covariant-contravariant refinement (CC-refinement) is a generalization of the notions of bisimulation and refinement, which is coinductively defined to describe behavior relation, i.e., two related processes are required to be always able to provide matched transitions each other. The notion of CC-n-refinement, where n is a natural number, presented in this paper, finitely approximates the notion of CC-refinement through weakening the above-mentioned requirement. A process is said to CC-n-refine another process whenever they can, within n-steps, match the transitions each other, and a CC-n-refinement relation may be considered to be a CC-refinement relation if n is big enough. Based on this kind of finite approximation, this paper presents CC-n-refinement modal logic (nCCRML) obtained from the modal system K by adding CC-n-refinement quantifiers, establishes an axiom system for nCCRML, and explores some important properties of this axiom system: soundness, completeness, and decidability. CC-n-refinement quantifiers can be used to formalize some interesting problems in the field of formal method.

Heyting-Lewis Logic is the extension of intuitionistic propositional logic with a strict implication connective that satisfies the constructive counterparts of axioms for strict implication provable in classical modal logics. Variants of this logic are surprisingly widespread: they appear as Curry-Howard correspondents of (simple type theory extended with) Haskellstyle arrows, in preservativity logic of Heyting arithmetic, in the proof theory of guarded (co)recursion, and in the generalization of intuitionistic epistemic logic. Heyting-Lewis Logic can be interpreted in intuitionistic Kripke frames extended with a binary relation to account for strict implication. We use this semantics to define descriptive frames (generalisations of Esakia spaces), and establish a categorical duality between the algebraic interpretation and the frame semantics. We then adapt a transformation by Wolter and Zakharyaschev to translate Heyting-Lewis Logic to classical modal logic with two unary operators. This allows us to prove a Blok-Esakia theorem that we then use to obtain both known and new canonicity and correspondence theorems, and the finite model property and decidability for a large family of Heyting-Lewis logics.

Perspective games model multi-agent systems in which agents can view only the parts of the system that they own. Unlike the observation-based model of partial visibility, where uncertainty is longitudinal – agents partially observe the full history, uncertainty in perspective games is transverse – agents fully observe parts of the history. So far, researchers studied zero-sum two-player perspective games. There, the objective of one agent (the system) is to satisfy a given specification, and the objective of the second agent (the environment) is to fail the specification.We study richer and more realistic settings of perspective games. We consider games with more than two players, and distinguish between zero-sum games, where the objectives of the players form a partition of all possible behaviors, zero-sum games among coalitions, where agents in a coalition share their objectives but do not share their visibility, and non-zero-sum games, where each agent has her own objectives and is assumed to be rational rather than hostile. In the non-zero-sum setting, we are interested in stable outcomes of the game; in particular, Nash equilibria.We show that, as is the case with longitudinal uncertainty, transverse uncertainty leads to undecidability in settings with three or more players that include coalitions or non-zero-sum objectives. We then focus on two-player non-zero-sum perspective games. There, finding and reasoning about stable outcomes is decidable, and in fact, unlike the case with longitudinal uncertainty, can be done in the same complexity as in games with full visibility. In particular, we study rational synthesis in the perspective setting, where the goal is to generate systems that satisfy their specification when interacting with rational environments. Our study includes Boolean objectives given by automata or LTL formulas, as well as a multi-valued setting, where the objectives are ${\text{LTL}}\left[ {\mathcal{F}} \right]$ formulas with satisfaction values in [0, 1], and the agents aim to maximize the satisfaction value of their objectives.

Symbolic finite transducers are extensions of classical finite transducers. A transition of a symbolic finite transducer represents a (possibly infinite) set of transitions of a classical one. This setting allows symbolic finite transducers to succinctly recognize transductions. A transducer is k-valued if the maximal number of different outputs for an input string is bounded by k and it is finite-valued if it is k-valued for some k. In this paper, we study the valuedness problem for symbolic finite transducers. We show that for symbolic finite transducers over decidable labels, the k-valuedness problem is decidable. For finite transducers, Weber introduced two criteria to characterize infinite-valuedness, both of which can be easily transformed into properties for symbolic finite transducers. Although these two criteria are sufficient conditions for infinite-valuedness, they are not necessary conditions however. As a result, a third criterion is introduced in order to completely characterize the infinite-valuedness of symbolic finite transducers.

Description logics are known to be a family of logic-based knowledge representation formalisms, and fuzzy description logics are expressive description logics for representing and handling fuzzy (vague or imprecise) knowledge bases. A sequential fuzzy description logic, which is introduced in this paper, is an extended fuzzy description logic where a sequence modal operator is introduced. In this paper, a translation from the proposed sequential fuzzy description logic to a standard fuzzy description logic is defined. Further, a theorem for embedding the sequential fuzzy description logic into the standard fuzzy description logic is proved using this translation. A theorem for relative decidability of the sequential fuzzy description logic with respect to the standard fuzzy description logic is established using the embedding theorem. The proposed logic and translation are intended for effective handling of fuzzy knowledge bases with sequential information (i.e., information expressed as sequences). Moreover, using the translation, existing methods and algorithms for the standard fuzzy description logic can be reused to effectively handle fuzzy knowledge bases with sequential information described by the sequential fuzzy description logic.

We study the computational complexity of existential Presburger arithmetic with (possibly nested occurrences of) a Kleene-star operator. In addition to being a natural extension of Presburger arithmetic, our investigation is motivated by two other decision problems. The first problem is the rational subset membership problem in graph groups. A graph group is an infinite group specified by a finite undirected graph. While a characterisation of graph groups with a decidable rational subset membership problem was given by Lohrey and Steinberg [J. Algebra, 320(2) (2008)], it has been an open problem (i) whether the decidable fragment has elementary complexity and (ii) what is the complexity for each fixed graph group. The second problem is the reachability problem for integer vector addition systems with states and nested zero tests. We prove that the satisfiability problem for existential Pres-burger arithmetic with stars is NEXP-complete and that all three problems are polynomially inter-reducible. Moreover, we consider for each problem a variant with a fixed parameter: We fix the star-height in the logic, a graph parameter for the membership problem, and the number of distinct zero-tests in the integer vector addition systems. We establish NP-completeness of all problems with fixed parameters. In particular, this enables us to obtain a complete description of the complexity landscape of the rational subset membership problem for fixed graph groups: If the graph is a clique, the problem is N L-complete. If the graph is a disjoint union of cliques, it is P-complete. If it is a transitive forest (and not a union of cliques), the problem is NP-complete. Otherwise, the problem is undecidable.

The $\mu$ -calculus with atoms, or nominal $\mu$ -calculus, is a temporal logic for reasoning about transition systems that operate on data atoms coming from an infinite domain and comparable only for equality. It is, however, not expressive enough to define some properties that are of interest from the perspective of system verification. To rectify this, we extend the calculus with tests for atom freshness with respect to the global history of transitions. Since global histories can grow arbitrarily large, it is not clear whether model checking for the extended calculus is decidable. We prove that it is, by showing that one can restrict attention only to locally relevant parts of the history.

A modal extension M4CC of Arieli, Avron, and Zamansky's ideal paraconsistent four-valued logic 4CC is introduced as a Gentzen-type sequent calculus. The completeness theorem with respect to a Kripke semantics for M4CC is proved. The finite model property for M4CC is shown by modifying the completeness proof. The decidability of M4CC is obtained as a corollary.

In this paper, a single-antecedent/succedent sequent calculus NL for first-order Nelsonian paraconsistent quantum logic is investigated. The logic under consideration is regarded as a combination of both Nelson's paraconsistent four-valued logic and Dalla Chiara and Giuntini's paraconsistent quantum logic. The duality and cut-elimination theorems for NL are proved. Decidability, some constructive properties, some constructible falsity properties, and Craig interpolation property are shown for NL. An extend NL with some naive comprehension rules in the naive set theory is also investigated.

In recent years, there has been an increasing interest in enriching the traditional control-flow perspective of processes with additional dimensions, the data perspective being the most prominent one. At the same time, variants of Petri nets with data have been extensively studied, giving raise to a plethora of formal models with different expressive power and computational guarantees. In this work, we focus on DPNs, a data-aware extension of P/T nets where the net is enriched with data variables of different types, and transitions are guarded by formulae that inspect and update such variables. Even though DPNs are less expressive than Petri nets where data are carried by tokens, they elegantly capture business processes operating over simple case data and taking complex decisions based on these data. Notably, various techniques have been implemented to discover DPNs from event data. However, such techniques do not guarantee that the discovered DPN is actually sound. In previous work, we have then studied how to check soundness of DPNs with simple data-based guards that can only compare variables with constants. In this paper, we generalize the study of soundness to DPNs to the fundamental case where the evolution of the process depends on the comparison between the values carried by different variables through linear inequations. Our main contribution is to show decidability of soundness for this sophisticated class of DPNs. This is done by constructing an abstract state space of the net relying on the manipulation of constraints, and by showing that such an abstract state space can be faithfully and effectively inspected for soundness. The construction lends itself to be directly implemented by combining standard state-space construction methods with constraint programming techniques.

Workflow nets (WF-nets) as a class of Petri nets are widely used to model and analyze workflow systems. Soundness is an important property of WF-nets, which guarantees that the systems are deadlock- and livelock-free and each task has a chance to be performed. Van der Aalst has proven that the soundness problem is decidable for WF-nets and we have also shown that it is PSPACE-complete for bounded ones. Since the definition of soundness is based on reachability and Van der Aalst has proven that a sound WF-net must be bounded, the soundness detection can be carried out via the reachability graph analysis. However, the state explosion problem is a big obstacle to this technique. The unfolding technique of Petri nets can effectively avoid/alleviate this problem. This paper proposes an algorithm to generate a finite prefix of the unfolding of a WF-net, called basic unfolding . Furthermore, a necessary and sufficient condition is proposed to decide soundness based on basic unfolding. In addition, some examples illustrate that the unfolding technique can save the storage space effectively.

We investigate the problem of decentralized fault prognosis of discrete-event systems modeled by unbounded labeled Petri nets. We assume that the system is monitored by a set of local agents (prognosers) with local observations so that they can predict the occurrence of fault in the system as a team. It is known in the literature that the notion of coprognosability provides the necessary and sufficient condition for the existence of a set of decentralized prognosers so that any fault can be predicted before its occurrence without false alarm. In this paper, we investigate the verification of coprognosability for systems modeled by labeled Petri nets. We show that coprognosability is decidable even when the Petri net is unbounded. Specifically, we provide an approach to transform the coprognosability verification problem to a model checking problem that can be effectively solved. Our result extends existing works on coprognosability analysis in decentralized fault prognosis from regular languages to Petri net languages.

Group anonymity, as an instance of information hiding, means that an agent is not identifiable within a group of agents with respect to an observer. In this paper we define group anonymity in security protocols by taking into account two types of observers: honest agents, as local observers of the protocol execution, and intruders (active or passive), as global observers of the protocol execution. It is shown that an action may be group anonymous in a protocol under a passive intruder but not in the same protocol under an active intruder, and vice versa. In case of basic-term actions, group anonymity in a protocol under an active intruder implies group anonymity in the same protocol under a passive intruder. A broad spectrum of relationships between group anonymity for various types of actions is developed, as well as relationships between group anonymity, minimal anonymity, and role interchangeability. Finally, the decidability and complexity status of the decision problems induced by these concepts is completely discussed. Thus, it is shown that group anonymity and role interchangeability are undecidable in unrestricted protocols. Group anonymity is complete for NEXPTIME when it is restricted to basic-term actions and bounded security protocols, and it is complete for NP when it is restricted to basic-term actions and L-session bounded security protocols.

Formalizing properties of systems with continuous dynamics is a challenging task. In this paper, we propose a formal framework for specifying and monitoring rich temporal properties of real-valued signals. We introduce signal first-order logic (SFO) as a specification language that combines first-order logic with linear-real arithmetic and unary function symbols interpreted as piecewise-linear signals. We first show that while the satisfiability problem for SFO is undecidable, its membership and monitoring problems are decidable. We develop an offline monitoring procedure for SFO that has polynomial complexity in the size of the input trace and the specification, for a fixed number of quantifiers and function symbols. We show that the algorithm has computation time linear in the size of the input trace for the important fragment of bounded-response specifications interpreted over input traces with finite variability. We can use our results to extend signal temporal logic with first-order quantifiers over time and value parameters, while preserving its efficient monitoring. We finally demonstrate the practical appeal of our logic through a case study in the micro-electronics domain.

The overwhelming and constantly growing amount of data network analysts have to process urges automated mechanisms for cyberthreat intelligence. The formal representation of network knowledge unifies data from diverse sources, and enables efficient automation via reasoning, however, network data is inherently uncertain and/or imprecise. There are various approaches to capture data certainty and vagueness, both at the level of abstraction and implementation, but many of these are not decidable, diverge from standards, and are limited in terms of querying and inference support. This paper proposes a description logic formalism to represent uncertain and fuzzy cyber-knowledge while keeping favorable computational properties and implementation concerns in mind. Refereed/Peer-reviewed

Our goal is to certify absence of information leaks in multi-agent workflows, such as conference management systems like EasyChair. These workflows can be executed by any number of agents some of which may form coalitions against the system. Therefore, checking noninterference is a challenging problem. Our paper offers two main contributions: First, a technique is provided to translate noninterference (in presence of various agent capabilities and declassification conditions) into universally quantified invariants of an instrumented new workflow program. Second, general techniques are developed for checking and inferring universally quantified inductive invariants for workflow programs. In particular, a large class of workflows is identified where inductiveness of invariants is decidable, as well as a smaller, still useful class of workflows where the weakest inductive universal invariant implying the desired invariant, is effectively computable. The new algorithms are implemented and applied to certify noninterference for workflows arising from conference management systems.

Recently, despite the growing popularity of smart contracts, one serious concern is arising among both industry and academia, that is, whether they work autonomously without human intervention really as intended and, when we are not sure, how we can ensure that contracts meet particular requirements. To resolve this, we propose a new formal approach to smart contract development: Instead of defining contracts just as programs in conventional languages, they should be defined using formal logic so that we can verify whether they meet particular requirements and enforce them if necessary. The primary challenge is that expressive formal logic often turns out to be undecidable and consequently executable programs cannot be generated. As a solution, each contract definition is divided into two layers, namely specification layer in a decidable logic called Linear Dynamic Logic for verification and enforcement of requirements and rule layer for defining implementation details, while the consistency between the two layers is systematically guaranteed. Based on this, it also becomes possible to automatically generate executable contract programs from their formal specification, which leads to improving the trustworthiness of contracts. Evaluation on Hyperledger Fabric shows the feasibility and high effectiveness of our approach.

Regarding the prominent threat of malware and the predicament faced by current identification technology, this paper considers that the primary reason is that the technical features used to identify malware are unstable and user-dependent. Furthermore, an in-depth analysis of those technical features leads us to believe that the root cause lies in the lag of discrimination theory behind practice. Because every piece of software has a specific task or purpose, we propose malware discrimination based on identifying the malicious tasks or purposes. We first present a formal definition of a task and then provide further classifications of malicious tasks. Then, based on decidable theory, we conclude that tasks are decidable, computable and finite, which enables us to prove that they are recursive and determinable. By establishing a map from software to task, we prove that software is many-to-one reducible to corresponding tasks. Thus, we show that software, including malware such as computer viruses, internet worms and Trojan horses, is also recursive and can be determined from the corresponding tasks. Finally, a discrimination process and practical examples are presented to verify our theory. Two key issues are identified for future research on malware discrimination.

The dot-depth hierarchy of Brzozowski and Cohen classifies the star-free languages of finite words. By a theorem of McNaughton and Papert, these are also the first-order definable languages. The dot-depth rose to prominence following the work of Thomas, who proved an exact correspondence with the quantifier alternation hierarchy of first-order logic: each level in the dot-depth hierarchy consists of all languages that can be defined with a prescribed number of quantifier blocks. One of the most famous open problems in automata theory is to settle whether the membership problem is decidable for each level: is it possible to decide whether an input regular language belongs to this level? Despite a significant research effort, membership by itself has only been solved for low levels. A recent breakthrough was achieved by replacing membership with a more general problem: separation. Given two input languages, one has to decide whether there exists a third language in the investigated level containing the first language and disjoint from the second. The motivation is that: (1) while more difficult, separation is more rewarding (2) it provides a more convenient framework (3) all recent membership algorithms are reductions to separation for lower levels. We present a separation algorithm for dot-depth two. While this is our most prominent application, our result is more general. We consider a family of hierarchies that includes the dot-depth: concatenation hierarchies. They are built via a generic construction process. One first chooses an initial class, the basis, which is the lowest level in the hierarchy. Further levels are built by applying generic operations. Our main theorem states that for any concatenation hierarchy whose basis is finite, separation is decidable for level one. In the special case of the dot-depth, this can be lifted to level two using previously known results.

We aim in this paper to integrate a nonmonotonic rule system (defeasible logic) with description logic-based ontologies. This can help us in building defeasible medical ontologies using vocabulary defined in description logic. We shall use defeasible reasoning to function on top of description logic. The process involves using the description logic system ALC to build a Disease-Symptom ontology. It also involves the addition of defeasible rules to an ALC knowledge base to achieve a flexible and decidable reasoning system which can be useful to clinician during medical diagnosis.

In the past few years, SAT-based methods in propositional logic have been widely used to tackle practical problems in electronic design automation, software testing and hardware verification. However, lots of industrial problems can naturally be transformed to certain decidable fragments of first-order logic (FOL), which are more expressive than propositional logic. In this paper, we propose a novel algorithm to compute all minimal unsatisfiable subsets for a constrained variant of first-order formulas. By this means, we not only evaluate the satisfiability of specified formulas, but also extract minimal unsatisfiable cores. A heuristic strategy is proposed to improve the performance. Experimental results demonstrate that our algorithm performs well on many industrial instances, and the heuristic strategy is more robust than other strategies in time and space efficiency.

We consider the hybridisations of the full branching time logic CTL* through the addition of nominals, binders and jumps. We formally define three fragments restricting the interplay between hybrid operators and path formulae contrary to previous proposals in the literature which ignored potential problems with a formal semantics. We then investigate the model checking problem for these logics obtaining complexities from PSPACE-completeness to non-elementary decidability.

We present decidability results for a sub-class of "non-interactive" simulation problems, a well-studied class of problems in information theory. A non-interactive simulation problem is specified by two distributions $P(x,y)$ and $Q(u,v)$: The goal is to determine if two players, Alice and Bob, that observe sequences $X^n$ and $Y^n$ respectively where $\{(X_i, Y_i)\}_{i=1}^n$ are drawn i.i.d. from $P(x,y)$ can generate pairs $U$ and $V$ respectively (without communicating with each other) with a joint distribution that is arbitrarily close in total variation to $Q(u,v)$. Even when $P$ and $Q$ are extremely simple: e.g., $P$ is uniform on the triples $\{(0,0), (0,1), (1,0)\}$ and $Q$ is a "doubly symmetric binary source", i.e., $U$ and $V$ are uniform $\pm 1$ variables with correlation say $0.49$, it is open if $P$ can simulate $Q$. In this work, we show that whenever $P$ is a distribution on a finite domain and $Q$ is a $2 \times 2$ distribution, then the non-interactive simulation problem is decidable: specifically, given $\delta > 0$ the algorithm runs in time bounded by some function of $P$ and $\delta$ and either gives a non-interactive simulation protocol that is $\delta$-close to $Q$ or asserts that no protocol gets $O(\delta)$-close to $Q$. The main challenge to such a result is determining explicit (computable) convergence bounds on the number $n$ of samples that need to be drawn from $P(x,y)$ to get $\delta$-close to $Q$. We invoke contemporary results from the analysis of Boolean functions such as the invariance principle and a regularity lemma to obtain such explicit bounds.

Well-structured pushdown systems (WSPDSs) extend pushdown systems with well-quasi-ordered (possibly in_nitely many) states and stack alphabet. As an expressive model for concurrent recursive computations, WSPDSs are believed to “be close the border of undecidability” [11]. Most of the decidability results are known only on subclasses. In this paper, we investigate the decidability of the termination and boundedness problems for WSPDSs using two algorithms: One is an extension of the reduced reachability tree technique proposed by Leroux et. al. in [11]. The other is based on Post^*-automata technique which has been successfully applied in the model checking of pushdown systems. The complexity of both are Hyper-Ackermannian for bounded WSPDSs. We implement both algorithms and make experiments on a large number of randomly generated WSPDSs. The results illustrate that the Post^*_automata based algorithm sometimes behaves an order of magnitude faster., リサーチレポート（北陸先端科学技術大学院大学先端科学技術研究科情報科学系）

The reachability problem is one of the most important issues in the verification of hybrid systems. But unfortunately the reachable sets for most of hybrid systems are not computable except for some special families. In our previous work, we identified a family of vector fields, whose state parts are linear with real eigenvalues, while input parts are exponential functions, and proved its reachability problem is decidable. In this paper, we investigate another family of vector fields, whose state parts are linear, but with pure imagine eigenvalues, while input parts are trigonometric functions, and prove its reachability problem is decidable also. To the best of our knowledge, the two families are the largest families of linear vector fields with a decidable reachability problem. In addition, we present an approach on how to abstract general linear dynamical systems to the first family. Comparing with existing abstractions for linear dynamical systems, experimental results indicate that our abstraction is more precise.

Description logics (DL) is a well-known knowledge representation formalism. DL have been applied as reasoning framework in diverse domains, including the Semantic Web and Context-Aware Systems. It is an open question whether or not the expressive description logic ALCQIOreg is decidable. This logic is equipped with negation, conjunction, regular roles, inverse roles, nominals and qualified number restrictions. In this paper, we show this logic is decidable when interpreted over tree models. Moreover, it is shown that μALCTIO, which is known to be undecidable and that subsumes ALCQIOreg, is in EXPTIME in the case of tree models. μALCTIO generalizes regular roles with fixed-point constructors, and qualified number restrictions with arithmetic constraints. This EXPTIME bound holds even if the arithmetic constraints are coded in binary. Furthermore, we show that knowledge base reasoning, TBoxes and ABoxes, can also be decided in EXPTIME. These results are achieved via a polynomial reduction to the satisfiability problem of the propositional modal i-calculus extended with Presburger arithmetic constraints interpreted over tree models.

Reliability Redundancy Allocation Problem (RRAP) in Wireless Sensor Network (WSN) system is obviously an important problem. The basic function of WSN system is to provide surveillance data transmission over a specified area maintaining minimum power consumption (minimum cost), occupying minimum volume and weight of system components with a reasonable level of reliability. In this paper, a decision making assessment of reliability of Redundancy Allocation Problem (RAP) is proposed using fuzzy approach. The fuzzy approach incurs the virtue of uncertainty in account to make the approach more practical. Triangular Fuzzy membership function is introduced to produce fuzzy number set as input variables (cost, weight and volume) to a hybrid optimization algorithm. The hybrid meta-heuristic algorithm aiming for reliability optimization in RAP of system components of WSN is discussed. This algorithm is based on a new hybrid algorithm using Genetic Algorithm (GA) and Particle Swarm Optimization (PSO). The fuzzy results obtained are used to exhibit decision making matrix to enhance decidability property of WSN. Finally after defuzzification crisp data are obtained and compared with other approaches from literature and found satisfactory.

Translocation is a useful operation on strings with challenging questions in combinatorics of permutations and interesting applications in analysis of sequences. A translocation operation essentially is the interchange of prefixes and suffixes among two substrings of a string. For the case of genomes represented as strings, symbols that represent genes and chromosomes are modeled as substrings of the genomes; thus, translocation is an operation that models the interaction between chromosomes inside a genome. The translocation distance between two genomes is defined as the minimum number of translocations to convert one genome into another and has been proved to be a meaningful manner of modeling the evolutive distance between organisms. The particular case of unsigned genomes, those in which the orientation of the genes are not considered, is particularly difficult, while the signed case, in which the orientation of genes is considered, has been proved to be polynomially decidable. This paper presents an innovative Genetic Algorithm (GA) approach to solve the unsigned translocation distance problem. A distinguishing feature of the proposed GA is that it uses as fitness function the translocation distance for randomly generated signed versions of the input (that is an unsigned genome). Experiments over randomly generated strings (synthetic genomes) showed that the proposed GA approach computes answers that are better than those computed by an L5+e-approximation algorithm, the latter also implemented as part of this work.

We adapt the 'mosaics' technique of Reynolds 1997 (in turn an adaption of Nemeti 1986) achieving decidability for the (non local) Ockhamist logic of (upward endless) bundled trees. We produce a double exponential time procedure, thus improving the complexity upper bound of the problem - so far relying on the non elementary procedure of the Rabin's Theorem (Burgess 1979).

In this talk, we survey recent results on situation calculus bounded action theories. These are action theories with the constraints that the size of the extension of fluents in every situation must be bounded, though such an extension changes from situation to situation. Such action theories give rise to infinite transition systems that can be faithfully abstracted into finite ones, making verification decidable.

Given a formula phi(x, X) positive in X, the bounded ness problem asks whether the fix point induced by phi is reached within some uniform bound independent of the structure (i.e. Whether the fix point is spurious, and can in fact be captured by a finite unfolding of the formula). In this paper, we study the bounded ness problem when phi is in the guarded fragment or guarded negation fragment of first-order logic, or the fix point extensions of these logics. It is known that guarded logics have many desirable computational and model theoretic properties, including in some cases decidable bounded ness. We prove that bounded ness for the guarded negation fragment is decidable in elementary time, and, making use of an unpublished result of Colcombet, even 2EXPTIME-complete. Our proof extends the connection between guarded logics and automata, reducing bounded ness for guarded logics to a question about cost automata on trees, a type of automaton with counters that assigns a natural number to each input rather than just a boolean.