Publications 2019

  1. Home
  2. Publications

Books


31.  Molecular logic and computational synthetic biology: first international symposium, MLCSB 2018, Santiago, Chile, December 17–18, 2018, Revised Selected Papers

Chaves, Madalena and Martins, Manuel A.

Springer

ria.ua.pt | doi

Book Chapters


30.  Reactive models for biological regulatory networks

Figueiredo, Daniel and Barbosa, Luís Soares

Molecular Logic and Computational Synthetic Biology: First International Symposium, MLCSB 2018, Santiago, Chile, December 17–18, 2018, Revised Selected Papers

Springer

A reactive model, as studied by D. Gabbay and his collaborators, can be regarded as a graph whose set of edges may be altered whenever one of them is crossed. In this paper we show how reactive models can describe biological regulatory networks and compare them to Boolean networks and piecewise-linear models, which are some of the most common kinds of models used nowadays. In particular, we show that, with respect to the identification of steady states, reactive Boolean networks lie between piecewise linear models and the usual, plain Boolean networks. We also show this ability is preserved by a suitable notion of bisimulation, and, therefore, by network minimisation.

ria.ua.pt | doi | Peer Reviewed

29.  Verification for Everyone? An Overview of Dynamic Logic

Madeira, Alexandre

Molecular Logic and Computational Synthetic Biology. MLCSB 2018. Lecture Notes in Computer Science

Springer

This note, reporting the homonym keynote presented in the International Symposium on Molecular Logic and Computational Synthetic Biology 2018, traces an informal roadmap on Dynamic Logic (DL) field, focusing on its versatility and resilience to be adjusted and adopted in a wide class of application domains and computational paradigms. The exposition argues the room for developments on tagging DL to the analysis of synthetic biologic domain.

ria.ua.pt | doi | Peer Reviewed

28.  A Hybrid Dynamic Logic for Event/Data-Based Systems

Hennicker, Rolf and Madeira, Alexandre and Knapp, Alexander

Lecture Notes in Computer Science - 22nd International Conference on Fundamental Approaches to Software Engineering, FASE 2019

Springer

We propose E↓ -logic as a formal foundation for the specification and development of event-based systems with local data states. The logic is intended to cover a broad range of abstraction levels from abstract requirements specifications up to constructive specifications. Our logic uses diamond and box modalities over structured actions adopted from dynamic logic. Atomic actions are pairs Open image in new window where e is an event and ? a state transition predicate capturing the allowed reactions to the event. To write concrete specifications of recursive process structures we integrate (control) state variables and binders of hybrid logic. The semantic interpretation relies on event/data transition systems; specification refinement is defined by model class inclusion. For the presentation of constructive specifications we propose operational event/data specifications allowing for familiar, diagrammatic representations by state transition graphs. We show that E↓-logic is powerful enough to characterise the semantics of an operational specification by a single E↓-sentence. Thus the whole development process can rely on E↓-logic and its semantics as a common basis. This includes also a variety of implementation constructors to support, among others, event refinement and parallel composition.

ria.ua.pt | doi | Peer Reviewed

27.  Rigid first-order hybrid logic

Blackburn, Patrick and Martins, Manuel and Manzano, María and Huertas, Antonia

Logic, Language, Information, and Computation. WoLLIC 2019. Lecture Notes in Computer Science

Springer Verlag

Hybrid logic is usually viewed as a variant of modal logic in which it is possible to refer to worlds. But when one moves beyond propositional hybrid logic to first- or higher-order hybrid logic, it becomes useful to view it as a systematic modal language of rigidification. The key point is this: @ can be used to rigidify not merely formulas, but other types of symbol as well. This idea was first explored in first-order hybrid logic (without function symbols) where @ was used to rigidify the firstorder constants. It has since been used in hybrid type-theory: here one only has function symbols, but they are of every finite type, and @ can rigidify any of them. This paper fills the remaining gap: it introduces a first-order hybrid language which handles function symbols, and allows predicate symbols to be rigidified. The basic idea is straightforward, but there is a slight complication: transferring information about rigidity between the level of terms and formulas. We develop a syntax to deal with this, provide an axiomatization, and prove a strong completeness result for a varying domain (actualist) semantics.

ria.ua.pt | doi | Peer Reviewed

26.  rPrism: a software for reactive weighted state transition models

Figueiredo, Daniel and Rocha, Eugénio and Martins, Manuel António and Chaves, Madalena

Hybrid Systems Biology

Springer, Cham

In this work we introduce the software rPrism, as a branch of the software PRISM model checker, in order to be able to study weighted reactive state transition models. This kind of model gathers together the concepts of reactivity { which consists of the capacity of a state transition model to alter its accessibility relation { and weights, which can be seen as costs, rates, etc.. Given a speci c model, the tool performs a simulation based on a Continuous Time Markov Chain. In particular, we show an example of its application for biological systems.

ria.ua.pt | doi | Peer Reviewed

25.  The educational math board game 3DM6

Almeida, M. R. and Barros, P. and Breda, A. and Resende, H. and Rocha, E.

EDULEARN19 Proceedings

IATED Digital Library

In this paper, we describe the conception and the difficulties behind the implementation of the three-dimensional and educational math game 3DM6 with features that make it engaging and suitable for different audiences. The 3DM6 game scope encompasses a school population attending three distinct levels of education that go from the 1st year of the 1st cycle to the 6th year of the 2nd cycle of the Portuguese Basic Education. Its fundamental purpose is to sharpen the curiosity of the players, integrating knowledge of various natures with special emphasis on mathematical knowledge. It includes both the general concept of a traditional board game and the main idea of a quiz, comprising features that differentiate it from a general game, among which are the learning opportunities resulting of the three-dimensional dynamics of the board where the game unfolds. The option by the design of a game in a 3D format took into account the barely inexistence of this type of game both in the commercial circuit and in the research field on serious games. Besides, and above all, this characteristic may bring a source of new learning opportunities acting also as a motivating agent making players feel more interested and engaged. There are several studies pointing to a possible relationship between games, including board games, and the development of spatial processing. However, little is known about the influence of 3D board games in the development of this type of capability or in any other math capability. At this stage of the 3DM6 game development, we have designed and implemented the physical structure of the game along with three distinct sets of card decks, taking into account the target audience and the goals to be achieved. Within this context, during the design phase, the incorporation of features to help players to acquire mathematical knowledge and/or to reinforce the learning of some specific academic contents were, as expected, taken into account. The math contents present in the game respects the curricular national programs of the Portuguese Basic Education and the proposed challenges have in consideration, essentially, the awakening or the development of the following capabilities: mental calculus, math reasoning, critical thinking and problem solving. The other contents are, basically, ludic and of historical and cultural nature.

ria.ua.pt | doi | Peer Reviewed

24.  A digital puzzle game for the elderly

Barros, P. and Almeida, M. R. and Breda, A. and Rocha, E.

EDULEARN19 Proceedings

IATED Digital Library

Several works in the literature show the importance that serious digital games have in maintaining the cognitive levels in the elderly population. However, there are important factors which limit their effective use, such as the game rules complexity and diversity, motivation and empathy with the tasks to be carried, users’ abilities to deal with technology (e.g. understanding the functionalities of a mouse device), physical limitations (e.g. mobility, reduced vision), psychological and mental limitations (e.g. reduced memory, social embarrassment), and behaviour limitations as neophobia (i.e. fear of newness or novelty). While addressing the previous factors, serious games need to find an adequate balance between the difficulty required in the game tasks and the user capabilities, in order to be able to maintain the elderly interest but still challenge their cognitive skills. Such implies that serious games for elderly people must have a clear and smooth way to tune the difficulty of the game level. Puzzle games seem to be good candidates for accomplishing the above requirements by changing the number of puzzle pieces, the number of allowed transformations (e.g. rotations, reflexions), colour stimulation, and/or theme selection of the puzzle images. Moreover, the rules are simple and intuitive, and there is a high probability that elderly people have already played some version of a puzzle. In this work, we describe the conception and difficulties behind the implementation of a digital puzzle game targeting the senior population, either institutionalized, being taken care at home, or living autonomously. It is well known that puzzle solving is a highly intensive mental process which strengthens mental fitness and slows the natural degradation process that comes with aging. In our proposed game, we tried not only to create an engaging experience but also, supported by scientific evidence, implement some features to train their mental abilities which are known to degrade over time; in an attempt to slow or even revert such degradation process. Also, since the game data is gathered with the informed consent of all the players, our second aim is to analyse the statistical data collected together with complementary medical information, in order to measure/determine some of the effects of playing digital puzzle games in the long term of mental degradation/fitness. The game is presented with a careful set of images from several sources. A preloaded gallery covers a wide range of popular themes (e.g. animals, nature, social gatherings) and targeting personal issues as the degree of visual impairment and cognitive/memory degradation. To promote further engagement, users can also customize the game experience by selecting themselves images from online resources (as google images) or images stored on their devices. Additionally, relatives or friends may remotely send images to the user’s account which may further promote their willing to play, if the images have some emotional connection attached. By saving data to a central server, caretakers can monitor the elderly activity and difficulties which may help to early diagnose their mental degradation. The proposed game was already used in 4 different elderly care centres, by more than 40 selected seniors with different profiles, in order to evaluate and benchmark the fulfilment of the work aims.

ria.ua.pt | doi | Peer Reviewed

23.  Logics for Petri nets with propagating failures

Gomes, Leandro and Madeira, Alexandre and Benevides, Mario

Fundamentals of Software Engineering. FSEN 2019. Lecture Notes in Computer Science

Springer International Publishing

Petri nets play a central role in the formal modelling of a wide range of complex systems and scenarios. Their ability to handle with both concurrency and resource awareness justifies their spread in the current formal development practices. On the logic side, Dynamic Logics are widely accepted as the de facto formalisms to reason about computational systems. However, as usual, the application to new situations raises new challenges and issues. The ubiquity of failures in the execution of current systems, interpreted in these models as triggered events that are not followed by the corresponding transition, entails not only the adjustment of these structures to deal with this reality, but also the introduction of new logics adequate to this emerging phenomenon. This paper contributes to this challenge by exploring a combination of two previous works of the authors, namely the Propositional Dynamic Logic for Petri Nets [1] and a parametric construction of multi-valued dynamic logics presented in [13]. This exercise results in a new family of Dynamic Logics for Petri Nets suitable to deal with firing failures.

ria.ua.pt | doi | Peer Reviewed

22.  Taming hierarchical connectors

Proença, José and Madeira, Alexandre

Fundamentals of Software Engineering. FSEN 2019. Lecture Notes in Computer Science

Springer

Building and maintaining complex systems requires good software engineering practices, including code modularity and reuse. The same applies in the context of coordination of complex component-based systems. This paper investigates how to verify properties of complex coordination patterns built hierarchically, i.e., built from composing blocks that are in turn built from smaller blocks. Most existing approaches to verify properties flatten these hierarchical models before the verification process, losing the hierarchical structure. We propose an approach to verify hierarchical models using containers as actions; more concretely, containers interacting with their neighbours. We present a dynamic modal logic tailored for hierarchical connectors, using Reo and Petri Nets to illustrate our approach. We realise our approach via a prototype implementation available online to verify hierarchical Reo connectors, encoding connectors and formulas into mCRL2 specifications and formulas.

ria.ua.pt | doi | Peer Reviewed

21.  On the generation of equational dynamic logics for weighted imperative programs

Gomes, Leandro and Madeira, Alexandre and Jain, Manisha and Barbosa, Luis S.

Formal Methods and Software Engineering. ICFEM 2019. Lecture Notes in Computer Science

Springer

Dynamic logic is a powerful framework for reasoning about imperative programs. This paper extends previous work [9] on the systematic generation of dynamic logics from the propositional to the equational case, to capture ‘full-fledged’ imperative programs. The generation process is parametric on a structure specifying a notion of ‘weight’ assigned to programs. The paper introduces also a notion of bisimilarity on models of the generated logics, which is shown to entail modal equivalence with respect to the latter.

ria.ua.pt | doi | Peer Reviewed

Articles


20.  Partial parking functions

Duarte, Rui and Guedes de Oliveira, António

Discrete Mathematics

Elsevier

We characterise the Pak-Stanley labels of the regions of a family of hyperplane arrangements that interpolate between the Shi arrangement and the Ish arrangement.

ria.ua.pt | doi | Peer Reviewed

19.  A Dawson-like clustering of human mitochondrial DNA sequences based on protein coding region

Soares, Inês and Duarte, Rui and Guedes de Oliveira, António and Amorim, António

Discrete Applied Mathematics

Elsevier

In the present paper, our main goal is focused in developing fast algorithms for human mtDNA sequence analyses, requiring minimum and explicit assumptions on mutation models and evolutionary pathways. We propose a new approach based on a construction of Dawson, a technique based on the ordering of the variable sites. In this approach, the first step corresponds to the computation of the order of the positions according to their capacity to separate the sequences into dichotomous groups. Aiming to avoid or at least to minimize the consideration of ambiguous evolutionary events such as insertions/deletions and recurrence, which cause well-known alignment problems, in the present study we only work with the protein coding sequence, the clearly more stable region in human mitochondrial genomes. This method was tested in a small set of 99 human mtDNA comprising representatives of all major haplogroups. The developed approach showed to be a choice to automate the clustering of human mtDNA sequences into broad groups, the output being in agreement with the canonical classification into macro-haplogroups deposited in the Phylotree database.

ria.ua.pt | doi | Peer Reviewed

18.  On interval dynamic logic: Introducing quasi-action lattices

Santiago, Regivan and Bedregal, Benjamín and Madeira, Alexandre and Martins, Manuel A.

Science of Computer Programming

Elsevier

In this paper we discuss the incompatibility between the notions of validity and impreciseness in the context of Dynamic Logics. To achieve that we consider the Łukasiewicz action lattice and its interval counterpart, we show how some validities fail in the context of intervals. In order to capture the properties of action lattices that remain valid for intervals we propose a new structure called Quasi-action Lattices which generalizes action lattices and is able to model both: The Łukasiewicz action lattice, Ł, and its interval counterpart, Łˆ. The notion of graded satisfaction relation is extended to quasi-action lattices. We demonstrate that, in the case of intervals, the relation of graded satisfaction is correct (cf. Theorem 3) with respect to the graded satisfaction relation on the Łukasiewicz action lattice. Although this theorem guarantees that satisfiability is preserved on intervals, we show that validity is not. We propose, then, to weaken the notion of validity on action lattices to designated validity on quasi-action lattices. In this context, Theorem 4 guarantees that the dynamic formulæ which are valid with respect to Ł will be designated valid with respect to Łˆ

ria.ua.pt | doi | Peer Reviewed

17.  On Herbrand’s Theorem for Hybrid Logic

Costa, Diana and Martins, Manuel and Marcos, João

Journal of Applied Logics – IfCoLog Journal of Logics and their Applications

Colege Publications

The original version of Herbrand’s theorem [8] for first-order logic provided the theoretical underpinning for automated theorem proving, by allowing a constructive method for associating with each first-order formula χ a sequence of quantifier-free formulas χ1, χ2, χ3, · · · so that χ has a first-order proof if and only if some χi is a tautology. Some other versions of Herbrand’s theorem have been developed for classical logic, such as the one in [6], which states that a set of quantifier-free sentences is satisfiable if and only if it is propositionally satisfiable. The literature concerning versions of Herbrand’s theorem proved in the context of non-classical logics is meager. We aim to investigate in this paper two versions of Herbrand’s theorem for hybrid logic, which is an extension of modal logic that is expressive enough so as to allow identifying specific sates of the corresponding models, as well as describing the accessibility relation that connects these states, thus being completely suitable to deal with relational structures [3]. Our main results state that a set of satisfaction statements is satisfiable in a hybrid interpretation if and only if it is propositionally satisfiable

ria.ua.pt | Peer Reviewed

16.  The number of parking functions with center of a given length

Duarte, Rui and Guedes de Oliveira, António

Advances in Applied Mathematics

Elsevier

Let 1≤r≤n and suppose that, when the Depth-first Search Algorithm is applied to a given rooted labeled tree on n+1 vertices, exactly r vertices are visited before backtracking. Let R be the set of trees with this property. We count the number of elements of R. For this purpose, we first consider a bijection, due to Perkinson, Yang and Yu, that maps R onto the set of parking function with center (defined by the authors in a previous article) of size r. A second bijection maps this set onto the set of parking functions with run r, a property that we introduce here. We then prove that the number of length n parking functions with a given run is the number of length n rook words (defined by Leven, Rhoades and Wilson) with the same run. This is done by counting related lattice paths in a ladder-shaped region. We finally count the number of length n rook words with run r, which is the answer to our initial question.

ria.ua.pt | doi | Peer Reviewed

15.  Gravitating solitons and black holes with synchronised hair in the four dimensional O(3) sigma-model

Herdeiro, C. and Perapechka, I. and Radu, E. and Shnir, Ya

Journal of High Energy Physics

Springer Verlag

We consider the O(3) non-linear sigma-model, composed of three real scalar fields with a standard kinetic term and with a symmetry breaking potential in four space-time dimensions. We show that this simple, geometrically motivated model, admits both self-gravitating, asymptotically flat, non-topological solitons and hairy black holes, when minimally coupled to Einstein’s gravity, without the need to introduce higher order kinetic terms in the scalar fields action. Both spherically symmetric and spinning, axially symmetric solutions are studied. The solutions are obtained under a ansatz with oscillation (in the static case) or rotation (in the spinning case) in the internal space. Thus, there is symmetry non-inheritance: the matter sector is not invariant under the individual spacetime isometries. For the hairy black holes, which are necessarily spinning, the internal rotation (isorotation) must be synchronous with the rotational angular velocity of the event horizon. We explore the domain of existence of the solutions and some of their physical properties, that resemble closely those of (mini) boson stars and Kerr black holes with synchronised scalar hair in Einstein-(massive, complex)-Klein-Gordon theory

ria.ua.pt | doi | Peer Reviewed

14.  Product preservation and stable units for reflections into idempotent subvarieties

Xarez, João José and Xarez, Isabel Andrade

Categories and General Algebraic Structures with Applications

Shahid Beheshti University, Tehran, Iran

We give a necessary and sufficient condition for the preservation of finite products by a reflection of a variety of universal algebras into an idempotent subvariety. It is also shown that simple and semi-left-exact reflections into subvarieties of universal algebras are the same. It then follows that a reflection of a variety of universal algebras into an idempotent subvariety has stable units if and only if it is simple and the above-mentioned condition holds.

ria.ua.pt | Peer Reviewed

13.  Optimal impulse control of dynamical systems

Piunovskiy, Alexey and Plakhov, Alexander and Torres, Delfim F. M. and Zhang, Yi

SIAM Journal on Control and Optimization

Using the tools of the Markov Decision Processes, we justify the dynamic programming approach to the optimal impulse control of deterministic dynamical systems. We prove the equivalence of the integral and differential forms of the optimality equation. The theory is illustrated by an example from mathematical epidemiology. The developed methods can be also useful for the study of piecewise deterministic Markov processes.

ria.ua.pt | Peer Reviewed

12.  Spherical tiling with GeoGebra

Breda, Ana and Santos, José dos

Resonance

Indian Academy of Sciences, Springer

The theory of spherical tilings is an interesting and fruitful field, attracting, among other researchers, mathematicians. It is a transverse topic crossing several mathematical areas such as geometry, algebra, topology and number theory, but it is also an object of interest for other scientific fields such as chemistry, physics, art and architecture. Here, we make use of GeoGebra to establish some results, describing a class of monohedral spherical tilings and inferring some conjectures. This will highlight how the use of this software has been crucial for the construction of new knowledge in mathematics with applications in different areas of engineering.

ria.ua.pt | doi | Peer Reviewed

11.  Balancing a static black ring with a phantom scalar field

Kleihaus, Burkhard and Kunz, Jutta and Radu, Eugen

Physics Letters B

Elsevier

All known five dimensional, asymptotically flat, static black rings possess conical singularities. However, there is no fundamental obstruction forbidding the existence of balanced configurations, and we show that the Einstein-Klein-Gordon equations admit (numerical) solutions describing static asymptotically flat black rings, which are regular on and outside the event horizon. The scalar field is 'phantom', which creates the self-repulsion necessary to balance the black rings. Similar solutions are likely to exist in other spacetime dimensions, the basic properties of a line element describing a four dimensional, asymptotically flat black ring geometry being discussed.

ria.ua.pt | doi | Peer Reviewed

10.  Completeness in Equational Hybrid Propositional Type Theory

Manzano, Maria and Martins, Manuel and Huertas, Antonia

Studia Logica

Springer Verlag

Equational Hybrid Propositional Type Theory (EHPTT) is a combination of propositional type theory, equational logic and hybrid modal logic. The structures used to interpret the language contain a hierarchy of propositional types, an algebra (a nonempty set with functions) and a Kripke frame. The main result in this paper is the proof of completeness of a calculus specifically defined for this logic. The completeness proof is based on the three proofs Henkin published last century: (i) Completeness in type theory (ii) The completeness of the first-order functional calculus and (iii) Completeness in propositional type theory. More precisely, from (i) and (ii) we take the idea of building the model described by the maximal consistent set; in our case the maximal consistent set has to be named, ♦- saturated and extensionally algebraic-saturated due to the hybrid and equational nature of EHPTT. From (iii), we use the result that any element in the hierarchy has a name. The challenge was to deal with all the heterogeneous components in an integrated system.

ria.ua.pt | doi | Peer Reviewed

9.  Charged black holes with axionic-type couplings: classes of solutions and dynamical scalarization

Fernandes, Pedro G. S. and Herdeiro, Carlos A. R. and Pombo, Alexandre M. and Radu, Eugen and Sanchis-Gual, Nicolas

Physical Review D

American Physical Society

We consider an augmented Einstein-Maxwell-scalar model including an axionic-type coupling between the scalar and electromagnetic field. We study dyonic black hole solutions in this model. For the canonical axionic coupling emerging from high energy physics, all charged black holes have axion hair. We present their domain of existence and investigate some physical properties. For other axionic-type couplings, two classes of black hole solutions may coexist in the model: scalar-free Reissner-Nordström black holes and scalarized black holes. We show that in some region of the parameter space the scalar-free solutions are unstable. Then, there is nonuniqueness since new scalarized black hole solutions with the same global charges, which are entropically preferred over the scalar-free solutions and, moreover, emerge dynamically from the instability of the former, also exist.

ria.ua.pt | doi | Peer Reviewed

8.  Einstein-Maxwell-scalar black holes: classes of solutions, dyons and extremality

Astefanesei, D. and Herdeiro, C. and Pombo, A. and Radu, E.

Journal of High Energy Physics

Springer Verlag

Spherical black hole (BH) solutions in Einstein-Maxwell-scalar (EMS) models wherein the scalar field is non-minimally coupled to the Maxwell invariant by some coupling function are discussed. We suggest a classification for these models into two classes, based on the properties of the coupling function, which, in particular, allow, or not, the ReissnerNordstr¨om (RN) BH solution of electrovacuum to solve a given model. Then, a comparative analysis of two illustrative families of solutions, one belonging to each class is performed: dilatonic versus scalarised BHs. By including magnetic charge, that is considering dyons, we show that scalarised BHs can have a smooth extremal limit, unlike purely electric or magnetic solutions. In particular, we study this extremal limit using the entropy function formalism, which provides insight on why both charges are necessary for extremal solutions to exist.

ria.ua.pt | doi | Peer Reviewed

7.  Spontaneously scalarized Kerr black holes in extended scalar-tensor-Gauss-Bonnet gravity

Cunha, Pedro V. P. and Herdeiro, Carlos A. R. and Radu, Eugen

Physical Review Letters

American Physical Society

We construct asymptotically flat, spinning, regular on and outside an event horizon, scalarized black holes (SBHs) in extended scalar-tensor-Gauss-Bonnet models. They reduce to Kerr BHs when the scalar field vanishes. For an illustrative choice of nonminimal coupling, we scan the domain of existence. For each value of spin, SBHs exist in an interval between two critical masses, with the lowest one vanishing in the static limit. Non-uniqueness with Kerr BHs of equal global charges is observed; the SBHs are entropically favoured. This suggests that SBHs form dynamically from the spontaneous scalarization of Kerr BHs, which are prone to a scalar-triggered tachyonic instability, below the largest critical mass. Phenomenologically, the introduction of BH spin damps the maximal observable difference between comparable scalarized and vacuum BHs. In the static limit, (perturbatively stable) SBHs can store over 20% of the spacetime energy outside the event horizon; in comparison with Schwarzschild BHs, their geodesic frequency at the ISCO can differ by a factor of 2.5 and deviations in the shadow areal radius may top 40%. As the BH spin grows, low mass SBHs are excluded, and the maximal relative differences decrease, becoming of the order of a few percent for dimensionless spin j≳0.5. This reveals a spin selection effect: non-GR effects are only significant for low spin. We discuss if and how the recently measured shadow size of the M87 supermassive BH constrains the length scale of the Gauss-Bonnet coupling.

ria.ua.pt | doi | Peer Reviewed

6.  Spontaneous scalarisation of charged black holes: coupling dependence and dynamical features

Fernandes, Pedro G. S. and Herdeiro, Carlos A. R. and Pombo, Alexandre M. and Radu, Eugen and Sanchis-Gual, Nicolas

Classical and Quantum Gravity

IOP Publishing

Spontaneous scalarisation of electrically charged, asymptotically flat Reissner–Nordström black holes (BHs) has been recently demonstrated to occur in Einstein–Maxwell–Scalar (EMS) models. This phenomenon is allowed by a non-minimal coupling between the scalar and the Maxwell fields, and does not require non-minimal couplings of the scalar field to curvature invariants. EMS BH scalarisation presents a technical simplification over the BH scalarisation that has been conjectured to occur in extended scalar–tensor Gauss–Bonnet (eSTGB) models. It is then natural to ask: (1) how universal are the conclusions extracted from the EMS model? And (2) how much do these conclusions depend on the choice of the non-minimal coupling function? Here we address these questions by performing a comparative analysis of several different forms for the coupling function including: exponential, hyperbolic, power-law and a rational function (fraction) couplings. In all of them we obtain and study the domain of existence of fundamental, spherically symmetric, scalarised BHs and compute, in particular, their entropy. The latter shows that scalarised EMS BHs are always entropically preferred over the RN BHs with the same total charge to mass ratio q. This contrasts with the case of eSTGB, where for the same power-law coupling the spherical, fundamental scalarised BHs are not entropically preferred over the Schwarzschild solution. Also, while the scalarised solutions in the EMS model for the exponential, hyperbolic and power-law coupling are very similar, the rational function coupling leads to a transition in the domain of existence, by virtue of a pole in the coupling function, into a region of 'exotic' solutions that violate the weak energy condition. Furthermore, fully non-linear dynamical evolutions of unstable RN BHs with different values of q are presented. These show: (1) for sufficiently small q, scalarised solutions with (approximately) the same q form dynamically; (2) for large q, spontaneous scalarisation visibly decreases q; thus evolutions are non-conservative; (3) despite the existence of non-spherical, static scalarised solutions, the evolution of unstable RN BHs under non-spherical perturbations leads to a spherical scalarised BH.

ria.ua.pt | doi | Peer Reviewed

5.  Nonlinear dynamics of spinning bosonic stars: formation and stability

Sanchis-Gual, N. and Di Giovanni, F. and Zilhão, M. and Herdeiro, C. and Cerdá-Durán, P. and Font, J. A. and Radu, E.

Physical Review Letters

American Physical Society

We perform numerical evolutions of the fully nonlinear Einstein (complex, massive) Klein-Gordon and Einstein (complex) Proca systems, to assess the formation and stability of spinning bosonic stars. In the scalar (vector) case these are known as boson (Proca) stars. Firstly, we consider the formation scenario. Starting with constraint-obeying initial data, describing a dilute, axisymmetric cloud of spinning scalar or Proca field, gravitational collapse toward a spinning star occurs, via gravitational cooling. In the scalar case the formation is transient, even for a nonperturbed initial cloud; a nonaxisymmetric instability always develops ejecting all the angular momentum from the scalar star. In the Proca case, by contrast, no instability is observed and the evolutions are compatible with the formation of a spinning Proca star. Secondly, we address the stability of an existing star, a stationary solution of the field equations. In the scalar case, a nonaxisymmetric perturbation develops, collapsing the star to a spinning black hole. No such instability is found in the Proca case, where the star survives large amplitude perturbations; moreover, some excited Proca stars decay to, and remain as, fundamental states. Our analysis suggests bosonic stars have different stability properties in the scalar (vector) case, which we tentatively relate to its toroidal (spheroidal) morphology. A parallelism with instabilities of spinning fluid stars is briefly discussed.

ria.ua.pt | doi | Peer Reviewed

4.  Epistemic logics with structured knowledge

Madeira, Alexandre and Martins, Manuel A. and Benevides, Mario R. F.

Electronic Notes in Theoretical Computer Science

Elsevier

Multi-agent Dynamic Epistemic Logic, as a suitable modal logic to reason about knowledge evolving systems, has emerged in a number of contexts and scenarios. The agents knowledge in this logic is simply characterised by valuations of propositions. This paper discusses the adoption of other richer structures to make these representations, as graphs, algebras or even epistemic models. This method of building epistemic logics over richer structures is called “Epistemisation”. On this view a parametric method to build such Epistemic Logics with Public Announcements is introduced. Moreover, a parametric notion of bisimulation is presented, and the modal invariance of the proposed logics, with respect to this relation, are proved. Some interesting application horizons opened with this construction are stated.

ria.ua.pt | doi | Peer Reviewed

3.  Generalising KAT to verify weighted computations

Gomes, Leandro and Madeira, Alexandre and Barbosa, Luis S.

Scientific Annals of Computer Science

Alexandru Ioan Cuza University of Iasi

Kleene algebra with tests (KAT) was introduced as an algebraic structure to model and reason about classic imperative programs, i.e. sequences of discrete transitions guarded by Boolean tests. This paper introduces two generalisations of this structure able to express programs as weighted transitions and tests with outcomes in non necessarily bivalent truth spaces: graded Kleene algebra with tests (GKAT) and a variant where tests are also idempotent (I-GKAT). In this context, and in analogy to Kozen’s encoding of Propositional Hoare Logic (PHL) in KAT we discuss the encoding of a graded PHL in I-GKAT and of its while-free fragment in GKAT. Moreover, to establish semantics for these structures four new algebras are defined: F SET (T ), F REL(K, T ) and F LANG(K, T ) over complete residuated lattices K and T , and M(n, A) over a GKAT or I-GKAT A. As a final exercise, the paper discusses some program equivalence proofs in a graded context.

ria.ua.pt | doi | Peer Reviewed

Proceedings


2.  New classes of monohedral spherical tilings by non-convex spherical hexagons and non-convex spherical Pentagons with GeoGebra

Breda, Ana and Santos, José Santos dos

34th International Conference on Computers and Their Applications - CATA 2019

In previous works we have ilustrate a procedure to obtain spherical tiling with GeoGebra. We have found new classes of monohedral spherical tiling by four spherical pentagons, and new class of dihedral spherical tiling by twelve spherical pentagons. One again, we would make use of GeoGebra to show how we can do generate new classes of monohedral non-convex hexagonal spherical tilings, H(C,τ), changing the side gluing rules of the regular spherical octahedral tiling, by local action of particular subgroups of spherical isometries. In relation to one of the new classes, by hexagonal tiles, we describe some of its properties. We also show the existence of a a new family of monohedral pentagonal tiling which arises as a degenarated case associated to the family H(C ,0) . All these classes of spherical tilings have emerged as a result of an interactive construction process, only possible by the use of newly produced GeoGebra tools and the dynamic interaction capabilities of this software.

ria.ua.pt | doi | Peer Reviewed

1.  On the importance of assessment on flipped learning

Descalço, Luís and Carvalho, Paula

EDULEARN19

IATED

We have been using a combination of computer systems in Calculus for some years. The system MEGUA on Sagemath for authoring parameterized contents, system SIACUA for helping autonomous learning with the parameterized contents created, with Bayesian feedback and finally PmatE, a computer system used in Portuguese national competitions, for doing the assessment. Although this combined use of the systems accomplishes one of our goals, to motivate study during the whole semester instead of only before the main tests, it does not seem to be enough to convince students to work before the classes in an inverted learning environment. Students tend to use the systems only before the assessment tests. In the academic year 2018/2019, we have confirmed this thesis. Although our effort to provide to students the best possible conditions for working before the classes, they correspond to this motivation only it this work is assessed in the beginning of the class. Hence, giving the materials and assuming they work is, at least in our context, an ineffective approach. We compare two topics in flipped learning in a course with 99 students of Industrial Management Engineering (IME): a topic where assessment took place in the beginning of the class with another one for which, there was no assessment in the beginning of the class. Moreover, we compare the performance of these students in IME with others of a similar sample, from other engineering courses, on the same topic in flipped learning. The first ones knew they would be evaluated by a mini-test and the later knew that they would not be subject to evaluation. Our main conclusion is that, at least in our context, it is not safe to assume students work seriously before classes in flipped learning. In the absence of intrinsic motivation, using assessment in the beginning of the class is the best approach to convince students to do the previous work. Also, in some simple topics, providing appropriate learning materials, including short videos, this approach can improve learning outcomes. The data we use include, computer systems usage data, student’s marks and interviews of IME students with the best final marks in the Calculus course.

ria.ua.pt | Peer Reviewed
(latest changes on 2020-04-20 20:39)

© 2019 CIDMA, all rights reserved