TY - JOUR AU - Beica, A. AU - Feret, J. AU - Petrov, T. TI - Tropical Abstraction of Biochemical Reaction Networks with Guarantees JF - ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE J2 - ELECTR NOTES COMPUT SCI VL - 350 PY - 2020 SP - 3 EP - 32 PG - 30 SN - 1571-0661 DO - 10.1016/j.entcs.2020.06.002 UR - https://m2.mtmt.hu/api/publication/33527404 ID - 33527404 LA - English DB - MTMT ER - TY - JOUR AU - Uustalu, T. AU - Veltri, N. AU - Zeilberger, N. TI - Eilenberg-Kelly Reloaded JF - ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE J2 - ELECTR NOTES COMPUT SCI VL - 352 PY - 2020 SP - 233 EP - 256 PG - 24 SN - 1571-0661 DO - 10.1016/j.entcs.2020.09.012 UR - https://m2.mtmt.hu/api/publication/33340064 ID - 33340064 N1 - Export Date: 23 November 2023 LA - English DB - MTMT ER - TY - JOUR AU - Bárcenas, Everardo AU - Lavalle-Martínez, José-de-Jesús AU - Molero-Castillo, Guillermo AU - Velázquez-Mena, Alejandro TI - A Note on Constructive Interpolation for the Multi-Modal Logic K JF - ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE J2 - ELECTR NOTES COMPUT SCI VL - 354 PY - 2020 SP - 3 EP - 16 PG - 14 SN - 1571-0661 DO - 10.1016/j.entcs.2020.10.002 UR - https://m2.mtmt.hu/api/publication/32638566 ID - 32638566 LA - English DB - MTMT ER - TY - JOUR AU - Chai, Xinwei AU - Ribeiro, Tony AU - Magnin, Morgan AU - Roux, Olivier AU - Inoue, Katsumi TI - Static Analysis and Stochastic Search for Reachability Problem JF - ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE J2 - ELECTR NOTES COMPUT SCI VL - 350 PY - 2020 SP - 139 EP - 158 PG - 20 SN - 1571-0661 DO - 10.1016/j.entcs.2020.06.008 UR - https://m2.mtmt.hu/api/publication/31764468 ID - 31764468 AB - This paper focuses on a major improvement on the analysis of reachability properties in large-scale dynamical biological models. To tackle such models, where classical model checkers fail due to state space explosion led by exhaustive search. Alternative static analysis approaches have been proposed, but they may also fail in certain cases due to non-exhaustive search. In this paper, we introduce a hybrid approach ASPReach, which combines static analysis and stochastic search to break the limits of both approaches. We tackle this issue on a modeling framework we recently introduced, Asynchronous Binary Automata Network (ABAN). We show that ASPReach is able to analyze efficiently some reachability properties which could not be solved by existing methods. We studied also various cases from biological literature, emphasizing the merits of our approach in terms of conclusiveness and performance. LA - English DB - MTMT ER - TY - JOUR AU - Kavanagh, Ryan TI - Parametrized Fixed Points and Their Applications to Session Types JF - ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE J2 - ELECTR NOTES COMPUT SCI VL - 352 PY - 2020 SP - 149 EP - 172 PG - 24 SN - 1571-0661 DO - 10.1016/j.entcs.2020.09.008 UR - https://m2.mtmt.hu/api/publication/31727720 ID - 31727720 AB - Parametrized fixed points are of particular interest to denotational semantics and are often given by "dagger operations" [10-12]. Dagger operations that satisfy the Conway identities [10] are particularly useful, because these identities imply a large class of identities used in semantic reasoning. We generalize existing techniques to define dagger operations on omega-categories and on O-categories. These operations enjoy a 2-categorical structure that implies the Conway identities. We illustrate these operators by considering applications to the semantics of session-typed languages. LA - English DB - MTMT ER - TY - JOUR AU - Dantas, Ana Paula dos Santos AU - de Souza, Cid Carvalho AU - Dias, Zanoni TI - A GRASP for the Convex Recoloring Problem in Graphs JF - ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE J2 - ELECTR NOTES COMPUT SCI VL - 346 PY - 2019 SP - 379 EP - 391 PG - 13 SN - 1571-0661 DO - 10.1016/j.entcs.2019.08.034 UR - https://m2.mtmt.hu/api/publication/32647800 ID - 32647800 N1 - Export Date: 24 May 2023 LA - English DB - MTMT ER - TY - JOUR AU - Campos, Victor AU - Lopes, Raul AU - Maia, Ana Karolinna AU - Sau, Ignasi TI - Adapting The Directed Grid Theorem into an FPT Algorithm JF - ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE J2 - ELECTR NOTES COMPUT SCI VL - 346 PY - 2019 SP - 229 EP - 240 PG - 12 SN - 1571-0661 DO - 10.1016/j.entcs.2019.08.021 UR - https://m2.mtmt.hu/api/publication/31576782 ID - 31576782 AB - Originally proved in 1986 by Robertson and Seymour, the Grid Theorem is one of the most important tools in the field of structural graph theory, finding numerous applications in the design of algorithms for undirected graphs. An analogous version of the Grid Theorem isn directed graphs was conjectured by Johnson et al. in 2001, and proved recently by Kawarabayashi and Kreutzer in 2015. Namely they showed that there is a function f (k) such that every directed graph of directed tree-width at least f (k) contains a cylindrical grid of size k as a butterfly minor. Moreover, they claim that their proof can be turned into an XP algorithm, with parameter k, that either constructs a decomposition of the appropriate width, or finds the claimed large cylindrical grid as a butterfly minor. In this article, we adapt some of the steps of the proof of Kawarabayashi and Kreutzer and we improve the XP algorithm into an FPT algorithm.The first step of the proof is an XP algorithm by Johnson et al. in 2001 that decides whether a directed graph D has directed tree-width at most 3k - 2 or admits a haven of order k. It is worth mentioning that a skecth of an FPT algorithm for this problem appears in Chapter 9 of the book "Classes of Directed Graphs", from 2018, with an approximation factor of 5k + 2. Our first contribution is to adapt the proof from Johnson et al. to find either an arboreal decomposition of width at most 3k - 2 or a haven of order k in a directed graph D in FPT time by making use of important separators. We then follow the roadmap of the proof by Kawarabayashi and Kreutzer by locally improving the complexity at some steps, in particular concerning the problem of finding hitting sets for brambles of large order. LA - English DB - MTMT ER - TY - JOUR AU - van der Weide, Niels AU - Geuvers, Herman TI - The Construction of Set-Truncated Higher Inductive Types JF - ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE J2 - ELECTR NOTES COMPUT SCI VL - 347 PY - 2019 SP - 261 EP - 280 PG - 20 SN - 1571-0661 DO - 10.1016/j.entcs.2019.09.014 UR - https://m2.mtmt.hu/api/publication/31202317 ID - 31202317 AB - We construct finitary set-truncated higher inductive types (HITs) from quotients and the propositional truncation. For that, we first define signatures as a modification of the schema by Basold et al., and we show they give rise to univalent categories of algebras in both sets and setoids. To interpret HITs, we use the well-known method of initial algebra semantics. The desired algebra is obtained by lifting the quotient adjunction to the level of algebras and adapting Dybjer's and Moeneclaey's interpretation of HITs in setoids. From this construction, we conclude that the equality types of HITs are freely generated and that HITs are unique. The results are formalized in the UniMath library. LA - English DB - MTMT ER - TY - JOUR AU - Dai, Y. AU - Foley, A.M. AU - Hoàng, C.T. ED - Coutinho, G. ED - Kohayakawa, Y. ED - Santos, V.d. ED - Urrutia, S. TI - On Coloring a Class of Claw-free Graphs JF - ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE J2 - ELECTR NOTES COMPUT SCI VL - 346 PY - 2019 SP - 369 EP - 377 PG - 9 SN - 1571-0661 DO - 10.1016/j.entcs.2019.08.033 UR - https://m2.mtmt.hu/api/publication/31134255 ID - 31134255 N1 - Conference code: 141508 Export Date: 20 January 2020 Funding details: Natural Sciences and Engineering Research Council of Canada, NSERC Funding text 1: This work was supported by the Canadian Tri-Council Research Support Fund. The 2nd and 3rd authors (A.M. Foley and C.T. Hoàng) were each supported by individual NSERC Discovery Grants. AB - Given a set L of graphs, a graph G is L-free if G does not contain any graph in L as an induced subgraph. Recently, Frédéric Maffray and co-authors showed that the problem of coloring {claw, 4K1, K5 \\ e}-free graphs can be solved in polynomial time. In this paper, we investigate a related class of graphs. A hole is an induced cycle of length at least 4. Two vertices x, y of a graph G are twins if for any vertex z different from x and y, xz is an edge if and only if yz is an edge. A hole-twin is the graph obtained from a hole by adding a vertex that forms a twin with some vertex of the hole. Hole-twins, and K5 \\ e, are interesting in their connection with line-graphs. They are among the forbidden subgraphs in the characterization of line-graphs. In this paper, we show there is a polynomial time algorithm to color (claw, 4K1, hole-twin)-free graphs. © 2019 The Author(s). LA - English DB - MTMT ER - TY - JOUR AU - Ibiapina, A. AU - Silva, A. ED - Coutinho, G. ED - Kohayakawa, Y. ED - Santos, V.d. ED - Urrutia, S. TI - Graphs with Girth at Least 8 are b-continuous JF - ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE J2 - ELECTR NOTES COMPUT SCI VL - 346 PY - 2019 SP - 677 EP - 684 PG - 8 SN - 1571-0661 DO - 10.1016/j.entcs.2019.08.059 UR - https://m2.mtmt.hu/api/publication/31134173 ID - 31134173 N1 - Conference code: 141508 Export Date: 20 January 2020 Funding details: Conselho Nacional de Desenvolvimento Científico e Tecnológico, CNPq, 401519/2016-3 Funding text 1: 1 Partially supported by CNPq Projects Universal no. 401519/2016-3 and Produtividade no. AB - A b-coloring of a graph is a proper coloring such that each color class has at least one vertex which is adjacent to each other color class. The b-spectrum of G is the set Sb(G) of integers k such that G has a b-coloring with k colors and b(G) = maxSb(G) is the b-chromatic number of G. A graph is b-continous if Sb(G)=[χ(G),b(G)]∩. An infinite number of graphs that are not b-continuous is known. It is also known that graphs with girth at least 10 are b-continuous. In this work, we prove that graphs with girth at least 8 are b-continuous, and that the b-spectrum of a graph G with girth at least 7 contains the integers between 2χ(G) and b(G). This generalizes a previous result by Linhares-Sales and Silva (2017), and tells that graphs with girth at least 7 are, in a way, almost b-continuous. © 2019 The Author(s). LA - English DB - MTMT ER -