@inproceedings{KSHP-sasb16,
  address = {Edinburgh, UK},
  month = sep,
  missingnumber = {2},
  missingvolume = {},
  series = {Electronic Notes in Theoretical Computer Science},
  publisher = {Elsevier Science Publishers},
  acronym = {{SASB}'16},
  booktitle = {{P}roceedings of {T}he {S}eventh {I}nternational {W}orkshop on {S}tatic {A}nalysis and {S}ystems {B}iology (SASB 2016)},
  title = {{Unfolding of Parametric Logical Regulatory Networks}},
  author = {Kolc{\'a}k, Juraj and {\v S}afr{\'a}nek, David and Haar, Stefan and Paulev{\'e}, Lo{\"i}c},
  year = {2016},
  note = {To appear},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KSHP-SASB16.pdf},
  url = {https://hal.archives-ouvertes.fr/hal-01354109},
  abstract = {In systems biology, models of cellular regulatory processes such as gene regulatory networks or signalling pathways are crucial to understanding the behaviour of living cells. Available biological data are however often insufficient for full model specification. In this paper, we focus on partially specified models where the missing information is abstracted in the form of parameters. We introduce a novel approach to analysis of parametric logical regulatory networks addressing both sources of combinatoric explosion native to the model. First, we introduce a new compact representation of admissible parameters using Boolean lattices. Then, we define the unfolding of parametric regulatory networks. The resulting structure provides a partial- order reduction of concurrent transitions, and factorises the common transitions among the concrete models. A comparison is performed against state-of-the-art approaches to parametric model analysis.}
}

@comment{{B-arxiv16,
  author =		Bollig, Benedikt, 
  affiliation = 	aff-LSVmexico,
  title =    		One-Counter Automata with Counter Visibility, 
  institution = 	Computing Research Repository, 
  number =    		1602.05940, 
  month = 		feb, 
  nmonth =     		2,
  year = 		2016, 
  type = 		RR, 
  axeLSV = 		mexico,
  NOcontrat = 		"",
  
  url =			http://arxiv.org/abs/1602.05940, 
  PDF =			"http://www.lsv.fr/Publis/PAPERS/PDF/B-arxiv16.pdf",
  lsvdate-new =  	20160222,
  lsvdate-upd =  	20160222,
  lsvdate-pub =  	20160222,
  lsv-category = 	"rapl",
  wwwpublic =    	"public and ccsb",
  note = 		18~pages, 

  abstract = "In a one-counter automaton (OCA), one can read a letter
    from some finite alphabet, increment and decrement the counter by
    one, or test it for zero. It is well-known that universality and
    language inclusion for OCAs are undecidable. We consider here OCAs
    with counter visibility: Whenever the automaton produces a letter,
    it outputs the current counter value along with~it. Hence, its
    language is now a set of words over an infinite alphabet. We show
    that universality and inclusion for that model are in PSPACE, thus
    no harder than the corresponding problems for finite automata, which
    can actually be considered as a special case. In fact, we show that
    OCAs with counter visibility are effectively determinizable and
    closed under all boolean operations. As~a~strict generalization, we
    subsequently extend our model by registers. The general nonemptiness
    problem being undecidable, we impose a bound on the number of
    register comparisons and show that the corresponding nonemptiness
    problem is NP-complete.",
}}

@inproceedings{HKP-vmcai2019,
  address = {Cascais/Lisbon, Portugal},
  month = jan,
  year = 2019,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Enea, Constantin and Piskac, Ruzica},
  acronym = {{VMCAI}'19},
  booktitle = {{P}roceedings of the 20th {I}nternational {C}onference on
   	       {V}erification, {M}odel {C}hecking and {A}bstract {I}nterpretation
	       ({VMCAI}'19)},
  author = {Haar, Stefan and Kolc{\'a}k, Juraj and Paulev{\'e}, Lo{\"i}c},
  title = {{Combining Refinement of Parametric Models with Goal-Oriented Reduction of Dynamics}},
  pages = {555-576},
  url = {https://hal.archives-ouvertes.fr/hal-01940174/},
  pdf = {https://hal.archives-ouvertes.fr/hal-01940174/file/manuscript.pdf},
  abstract = {Parametric models abstract part of the specification of dynamical models by integral parameters. They are for example used in computational systems biology, notably with parametric regulatory networks, which specify the global architecture (interactions) of the networks, while parameterising the precise rules for drawing the possible temporal evolutions of the states of the components. A key challenge is then to identify the discrete parameters corresponding to concrete models with desired dynamical properties. This paper addresses the restriction of the abstract execution of parametric regulatory (discrete) networks by the means of static analysis of reachability properties (goal states). Initially defined at the level of concrete parameterised models, the goal-oriented reduction of dynamics is lifted to parametric networks, and is proven to preserve all the minimal traces to the specified goal states. It results that one can jointly perform the refinement of parametric networks (restriction of domain of parameters) while reducing the necessary transitions to explore and preserving reachability properties of interest.}
}

@techreport{CHKTP-hal18,
  author = {Chatain, {\relax Th}omas and Haar, Stefan and Kolc{\'a}k, Juraj and Thakkar, Aalok and Paulev{\'e}, Lo{\"i}c},
  institution = {HAL},
  month = oct,
  note = {33~pages},
  number = {hal-01893106},
  type = {Research Report},
  title = {{Concurrency in Boolean networks}},
  year = {2018},
  url = {https://hal.inria.fr/hal-01893106},
  pdf = {https://hal.inria.fr/hal-01893106/document},
  abstract = {Boolean networks (BNs) are widely used to model the qualitative dynamics of biological systems. Besides the logical rules determining the evolution of each component with respect to the state of its regulators, the scheduling of components updates can have a dramatic impact on the predicted behaviours. In this paper, we explore the use of Contextual Petri Nets (CPNs) to study dynamics of BNs with a concurrency theory perspective. After showing bi-directional translations between CPNs and BNs and analogies between results on synchronism sensitivies, we illustrate that usual updating modes for BNs can miss plausible behaviours, i.e., incorrectly conclude on the absence/impossibility of reaching specific configurations. Taking advantage of CPN semantics enabling more behaviour than the generalized asynchronous updating mode, we propose an encoding of BNs ensuring a correct abstraction of any multivalued refinement, as one may expect to achieve when modelling biological systems with no assumption on its time features.}
}

@article{KSHP-tcs19,
  publisher = {Elsevier Science Publishers},
  journal = {Theoretical Computer Science},
  author = {Kolc{\'a}k, Juraj and {\v S}afr{\'a}nek, David and Haar, Stefan and Paulev{\'e}, Lo{\"i}c},
  title = {{Parameter Space Abstraction and Unfolding Semantics of Discrete Regulatory Networks}},
  volume = {765},
  year = {2019},
  pages = {120-144},
  doi = {10.1016/j.tcs.2018.03.009},
  pdf = {https://hal.archives-ouvertes.fr/hal-01734805/document},
  url = {https://hal.archives-ouvertes.fr/hal-01734805/},
  abstract = {The modelling of discrete regulatory networks combines a graph specifying the pairwise influences between the variables of the system, and a parametrisation from which can be derived a discrete transition system. Given the influence graph only, the exploration of admissible parametrisations and the behaviours they enable is computationally demanding due to the combinatorial explosions of both parametrisation and reachable state space. This article introduces an abstraction of the parametrisation space and its refinement to account for the existence of given transitions, and for constraints on the sign and observability of influences. The abstraction uses a convex sub-lattice containing the concrete parametrisation space specified by its infimum and supremum parametrisations. It is shown that the computed abstractions are optimal, i.e., no smaller convex sublattice exists. Although the abstraction may introduce over-approximation, it has been proven to be conservative with respect to reachability of states. Then, an unfolding semantics for Parametric Regulatory Networks is defined, taking advantage of concurrency between transitions to provide a compact representation of reachable transitions. A prototype implementation is provided: it has been applied to several examples of Boolean and multi-valued networks, showing its tractability for networks with numerous components.}
}

@article{CHKPT-nc19,
  publisher = {Springer},
  journal = {Natural Computing},
  author = {Chatain, {\relax Th}omas and Haar, Stefan and Kolc{\'a}k, Juraj and Paulev{\'e}, Lo{\"i}c and Thakkar, Aalok},
  title = {Concurrency in {Boolean} networks},
  volume = {19},
  pages = {91--109},
  year = 2020,
  pdf = {https://hal.inria.fr/hal-01893106v2/document},
  url = {https://link.springer.com/article/10.1007/s11047-019-09748-4},
  abstract = {Boolean networks (BNs) are widely used to model the qualitative dynamics
of biological systems. Besides the logical rules determining the evolution of each
component with respect to the state of its regulators, the scheduling of component
updates can have a dramatic impact on the predicted behaviours. In this paper, we
explore the use of Read (contextual) Petri Nets (RPNs) to study dynamics of BNs from
a concurrency theory perspective. After showing bi-directional translations between
RPNs and BNs and analogies between results on synchronism sensitivity, we illustrate
that usual updating modes for BNs can miss plausible behaviours, i.e., incorrectly
conclude on the absence/impossibility of reaching specific configurations. We propose
an encoding of BNs capitalizing on the RPN semantics enabling more behaviour than the
generalized asynchronous updating mode. The proposed encoding ensures a correct
abstraction of any multivalued refinement, as one may expect to achieve when modelling
biological systems with no assumption on its time features.}
}

@article{PKCH-natcommun20,
  publisher = {Nature Research},
  journal = {Nature Communications},
  author = {Lo{\"i}c Paulev{\'e} and Juraj Kolc{\'a}k and Thomas Chatain and Stefan Haar},
  title = {Reconciling qualitative, abstract, and scalable modeling of biological networks},
  volume = {11},
  number = {4256},
  month = aug,
  doi = {10.1038/s41467-020-18112-5},
  year = {2020},
  url = {https://www.nature.com/articles/s41467-020-18112-5}
}

@inproceedings{KDHKSY-tacas2020,
  address = {Dublin, Ireland},
  month = apr,
  volume = {12078},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Armin Biere and David Parker},
  acronym = {{TACAS}'20},
  booktitle = {{P}roceedings of the 26th {I}nternational 
               {C}onference on {T}ools and {A}lgorithms for
               {C}onstruction and {A}nalysis of {S}ystems
               ({TACAS}'20)},
  author = {Juraj Kolc{\'a}k and J{\'e}r{'e}my Dubut and Ichiro Hasuo and Shin-Ya Katsumata and David Sprunger and Akihisa Yamada},
  title = {Relational Differential Dynamic Logic},
  pages = {191--208},
  doi = {10.1007/978-3-030-45190-5_11},
  year = 2020,
  url = {https://doi.org/10.1007/978-3-030-45190-5_11}
}

This file was generated by bibtex2html 1.98.