1,720,993 research outputs found
MAPmAKER: Performing multi-robot LTL planning under uncertainty
No full textRobot applications are being increasingly used in real life to help humans performing dangerous, heavy, and/or monotonous tasks. They usually rely on planners that given a robot or a team of robots compute plans that specify how the robot(s) can fulfill their missions. Current robot applications ask for planners that make automated planning possible even when only partial knowledge about the environment in which the robots are deployed is available. To tackle such challenges we developed MAPmAKER, which provides a decentralized planning solution and is able to work in partially known environments. Decentralization is realized by decomposing the robotic team into subteams based on their missions, and then by running a classical planning algorithm. Partial knowledge is handled by calling several times a classical planning algorithm. Demo video available at: https://youtu.be/TJzC_u2yfzQ
COVER: Change-based goal verifier and reasoner
No full textCOVER is a unified framework that supports the interplay between requirements analysts and software developers. It contracts a bridge between the requirements analyst's and the software developer's artifacts by enabling goal model analysis during software design. The goal model produced by the requirements analyst is kept alive and updated while the system is designed. Whenever the design of the system changes, COVER verifies the new design against the requirements of interest. The verification results are used to trigger a goal model analysis procedure. The results of this analysis can be used by the requirements analyst and the software developer to update the goal model or the design of the system. In this paper, we present the tool support developed for COVER
Integrating topological proofs with model checking to instrument iterative design
Full text linkSystem development is not a linear, one-shot process. It proceeds through refinements and revisions. To support assurance that the system satisfies its requirements, it is desirable that continuous verification can be performed after each refinement or revision step. To achieve practical adoption, formal verification must accommodate continuous verification efficiently and effectively. Model checking provides developers with information useful to improve their models only when a property is not satisfied, i.e., when a counterexample is returned. However, it is desirable to have some useful information also when a property is instead satisfied. To address this problem we propose TOrPEDO, an approach that supports verification in two complementary forms: model checking and proofs. While model checking is typically used to pinpoint model behaviors that violate requirements, proofs can instead explain why requirements are satisfied. In our work, we introduce a specific notion of proof, called Topological Proof. A topological proof produces a slice of the original model that justifies the property satisfaction. Because models can be incomplete, TOrPEDO supports reasoning on requirements satisfaction, violation, and possible satisfaction (in the case where satisfaction depends on unknown parts of the model). Evaluation is performed by checking how topological proofs support software development on 12 modeling scenarios and 15 different properties obtained from 3 examples from literature. Results show that: (i) topological proofs are 60% smaller than the original models; (ii) after a revision, in 78% of cases, the property can be re-verified by relying on a simple syntactic check
TOrPEDO: witnessing model correctness with topological proofs
Full text linkModel design is not a linear, one-shot process. It proceeds throughrefinements and revisions. To effectively support developers ingenerating model refinements and revisions, it is desirable to havesome automated support to verify evolvable models. To address thisproblem, we recently proposed to adopt topological proofs,which are slices of the original model that witness propertysatisfaction. We implemented TOrPEDO, a framework that providesautomated support for using topological proofs during model design.Our results showed that topological proofs are significantly smallerthan the original models, and that, in most of the cases, they allowthe property to be re-verified by relying only on a simple syntacticcheck. However, our results also show that the procedure thatcomputes topological proofs, which requires extracting unsatisfiablecores of LTL formulae, is computationally expensive. For thisreason, TOrPEDO currently handles models with a small dimension. Withthe intent of providing practical and efficient support for flexiblemodel design and wider adoption of our framework, in this paper, wepropose an enhanced—re-engineered—version of TOrPEDO. The newversion of TOrPEDO relies on a novel procedure to extracttopological proofs, which has so far represented the bottleneck ofTOrPEDO performances. We implemented our procedure within TOrPEDO byconsidering Partial Kripke Structures (PKSs) and Linear-timeTemporal Logic (LTL): two widely used formalisms to express modelswith uncertain parts and their properties. To extract topologicalproofs, the new version of TOrPEDO converts the LTL formulae into anSMT instance and reuses an existing SMT solver (e.g., MicrosoftZ3) to compute an unsatisfiable core. Then, theunsatisfiable core returned by the SMT solver is automaticallyprocessed to generate the topological proof. We evaluated TOrPEDO byassessing (i) how does the size of the proofs generated by TOrPEDOcompares to the size of the models being analyzed; and (ii) howfrequently the use of the topological proof returned by TOrPEDOavoids re-executing the model checker. Our results show that TOrPEDOprovides proofs that are smaller (≈ 60%) than theirrespective initial models effectively supporting designers increating model revisions. In a significant number of cases (≈ 79%), the topological proofs returned by TOrPEDO enable assessingthe property satisfaction without re-running the model checker. Weevaluated our new version of TOrPEDO by assessing (i) how it comparesto the previous one; and (ii) how useful it is in supporting theevaluation of alternative design choices of (small) model instancesin applied domains. The results show that the new version of TOrPEDOis significantly more efficient than the previous one and cancompute topological proofs for models with less than 40 stateswithin two hours. The topological proofs and counterexamplesprovided by TOrPEDO are useful to support the development ofalternative design choices of (small) model instances in applieddomains
High-level mission specification for multiple robots
No full textMobile robots are increasingly used in our everyday life to autonomously realize missions. A variety of languages has been proposed to support roboticists in the systematic development of robotic applications, ranging from logical languages with well-defined semantics to domain-specific languages with user-friendly syntax. The characteristics of both of them have distinct advantages, however, developing a language that combines those advantages remains an elusive task. We present PROMISE, a novel language that enables domain experts to specify missions on a high level of abstraction for teams of autonomous robots in a user-friendly way, while having well-defined semantics. Our ambition is to permit users to specify high-level goals instead of a series of specific actions the robots should perform. The language contains a set of atomic tasks that can be executed by robots and a set of operators that allow the composition of these tasks in complex missions. The language is supported by a standalone tool that permits mission specification through a textual and a graphical interface and that can be integrated within a variety of frameworks. We integrated PROMISE with a software platform providing functionalities such as motion control and planning. We conducted experiments to evaluate the correctness of the specification and execution of complex robotic missions with both simulators and real robots. We also conducted two user studies to assess the simplicity of PROMISE. The results show that PROMISE effectively supports users to specify missions for robots in a user-friendly manner
Going Beyond Counting First Authors in Author Co-citation Analysis
Full text linkThe present study examines one of the fundamental aspects of author co-citation analysis (ACA) - the way co-citation
counts are defined. Co-citation counting provides the data on which all subsequent statistical analyses and mappings
are based, and we compare ACA results based on two different types of co-citation counting - the traditional type that
only counts the first one among a cited work's authors on the one hand and a non-traditional type that takes into
account the first 5 authors of a cited work on the other hand. Results indicate that the picture produced through this non-traditional author co-citation counting contains more coherent author groups and is therefore considerably clearer. However, this picture represents fewer specialties in the research field being studied than that produced through the traditional first-author co-citation counting when the same number of top-ranked authors is selected and analyzed. Reasons for these effects are discussed
Dealing with incompleteness in automata-based model checking
No full textA software specification is often the result of an iterative process that transforms an initial incomplete model through refinement decisions. A model is incomplete because the implementation of certain functionalities is postponed to a later development step or is delegated to third parties. An unspecified functionality may be later replaced by alternative solutions, which may be evaluated to analyze tradeoffs. Model checking has been proposed as a technique to verify that a model of the system under development is compliant with a formal specification of its requirements. However, most classical model checking approaches assume that a complete model of the system is given: they do not support incompleteness. A verification-driven design process would instead benefit from the ability to apply formal verification at any stage, hence also to incomplete models. After any change, it is desirable that only the portion affected by the change, called replacement, is analyzed. To achieve this goal, this paper extends the classical automata-based model checking procedure to deal with incompleteness. The proposed model checking approach is able not only to evaluate whether a property definitely holds, possibly holds or does not hold in an incomplete model but, when the satisfaction of the specification depends on the incomplete parts, to compute the constraints that must be satisfied by their future replacements. Constraints are properties on the unspecified components that, if satisfied by the replacement, guarantee the satisfaction of the original specification in the refined model. Each constraint is verified in isolation on the corresponding replacement
Variations on the Author
Full text link“Variations on the Author” discusses two of Eduardo Coutinho’s recent films (Um Dia na Vida, from 2010, and Últimas Conversas, posthumously released in 2015) and their contribution to the general question of documentary authorship. The director’s filmography is characterized by a consistent yet self-effacing form of authorial self-inscription: Coutinho often features as an interviewer that rather than express opinions propels discourses; an interviewer that is good at listening. This mode of self-inscription characterizes him as an author who is not expressive but who is nonetheless markedly present on the screen. In Um Dia na Vida, however, Coutinho is completely absent form the image, while Últimas Conversas, on the contrary, includes a confessional prologue that moves the director from the margins to the center of his films. This article examines the ways in which these works stand out in the filmography of a director who offers new insights into the notion of cinematic authorship
Appropriate Similarity Measures for Author Cocitation Analysis
Full text linkWe provide a number of new insights into the methodological discussion about author cocitation analysis. We first argue that the use of the Pearson correlation for measuring the similarity between authors’ cocitation profiles is not very satisfactory. We then discuss what kind of similarity measures may be used as an alternative to the Pearson correlation. We consider three similarity measures in particular. One is the well-known cosine. The other two similarity measures have not been used before in the bibliometric literature. Finally, we show by means of an example that our findings have a high practical relevance.information science;Pearson correlation;cosine;similarity measure;author cocitation analysis
- …
