Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: deprecated: our papers

Topic: Yoneda Hacking: The Algebra of Attacker Actions

Georgios Bakirtzis (Mar 02 2021 at 14:37):

Here is the second paper (this time with @Fabrizio Genovese and C. Fleming) that implements model-based security analysis compositionally. Any comments welcome given that we are still under review and can make changes https://arxiv.org/abs/2103.00044

Jade Master (Mar 02 2021 at 16:14):

20210228_184714.jpg

Jade Master (Mar 02 2021 at 16:14):

The title reminds me of this meme:

Georgios Bakirtzis (Mar 02 2021 at 16:38):

lol true, blame fabrizio and cody for the yoneda hacking part :P

Georgios Bakirtzis (Mar 07 2021 at 23:39):

@Bruno Gavranovic I saw your tweet (although I am not on twitter). We should talk I am already moving towards a similar direction, I was going to talk about this with @Fabrizio Genovese when I had something concrete but if people are thinking about this already it might be worth it to have a chat

Fabrizio Genovese (Mar 08 2021 at 00:43):

Let's talk about this!

Bruno Gavranović (Mar 08 2021 at 00:56):

I'm down!

Spencer Breiner (Mar 08 2021 at 17:13):

Hi @Giorgos Bakirtzis @Fabrizio Genovese

I'm reading through this paper and having some trouble attaching intuitions to the mathematics. Specifically, I'd like to hear more about the representation of a system (?) as a functor $\mathbf{W}\to\mathbf{Cat}$.

I don't have a good sense of what the semantics are supposed to be here. Is this supposed to be something like behaviors through time, with composition by concatenation at common states? Thanks!

Fabrizio Genovese (Mar 08 2021 at 17:41):

Nope, to each box you are attaching the category of all possible things that can inhabit the box. So it's not like "To a box I attach one system". It's more like "to a box I attach the category of systems that can inhabit it"

Fabrizio Genovese (Mar 08 2021 at 17:43):

Then, as you compose boxes, you obtain a functor between categories that tells you something along the lines of:
"You are attaching a category C to X and a category D to Y. IF you have a morphism X -f-> Y, then a given system S in C will be mapped to a system FfS in Y"

Georgios Bakirtzis (Mar 08 2021 at 17:43):

Maybe we should say that in the paper

Spencer Breiner (Mar 08 2021 at 18:20):

Fabrizio Genovese said:

Nope, to each box you are attaching the category of all possible things that can inhabit the box. So it's not like "To a box I attach one system". It's more like "to a box I attach the category of systems that can inhabit it"

I understand that we're interested in a "universe of interest" rather than a particular system, but what are the elements of that universe (in some naive example)? The "things that can inhabit" are viewed as the objects or the arrows of the category?

Spencer Breiner (Mar 08 2021 at 18:22):

Put another way, if the box-fillers are the objects, what are the arrows (and composition)? If the box-fillers are arrows, what are the objects (and composition)?

Spencer Breiner (Mar 08 2021 at 18:25):

I'm really trying to understand this definition better:
"A system is a pair $(X, S)$, with $X$ an object of $\bf{W}$ and $S$ an object of $FX$."
So $X$ tells me the interface, and $S$ is supposed to characterize the system somehow, but I want to get a better sense of what that looks like.

Fabrizio Genovese (Mar 08 2021 at 18:27):

Spencer Breiner said:

I'm really trying to understand this definition better:
"A system is a pair $(X, S)$, with $X$ an object of $\bf{W}$ and $S$ an object of $FX$."
So $X$ tells me the interface, and $S$ is supposed to characterize the system somehow, but I want to get a better sense of what that looks like.

So, the objects of the category are the possible inhabitants of the box. Since to do what we do in the paper we have to pinpoint one specific system, I say that a system is a couple like the one you wrote down, that is, a box, and an object in the category to which we map the box

Spencer Breiner (Mar 08 2021 at 18:28):

But then what are the arrows?

Fabrizio Genovese (Mar 08 2021 at 18:28):

The morphism are just the possible ways to transform the systems that inhabit the box. For instance, you can map a box with m inputs and n outputs to the category of Mealy machines with m inputs and n outputs. The arrows of this categories are ways to transform these Mealy machines one into the other

Fabrizio Genovese (Mar 08 2021 at 18:29):

The existence of those arrows is exactly what allows Yoneda Hacking to make sense!

Spencer Breiner (Mar 08 2021 at 18:33):

Ordinarily I would think of the "category of Mealy machines" to have interfaces as objects and machines as arrows. I'm a bit fuzzy on the details, but I think there are 2-arrows that modulate internal state spaces (maybe without changing observable behavior?). Should I be thinking about a value categories $FX$ here as being a Hom-category in a 2-category?

Fabrizio Genovese (Mar 08 2021 at 18:38):

I think you could, possibly. I do agree that usually you expect the interfaces to be the objects, but this framework is a bit different. In any case this stuff is given for granted in this paper, it is probably better to read something else first (I guess it's in the references, but @Giorgos Bakirtzis knows better than me where to look)

Jade Master (Mar 09 2021 at 01:25):

Not sure if this will help, but it looks like systems are objects of the Grothendieck construction $\int F$ of $F : W \to Cat$. Is that right?

Joe Moeller (Mar 09 2021 at 01:52):

I was thinking the same Jade. Is it actually section 5.5 in Monoidal Grothendieck construction?

Fabrizio Genovese (Mar 09 2021 at 09:15):

Jade Master said:

Not sure if this will help, but it looks like systems are objects of the Grothendieck construction $\int F$ of $F : W \to Cat$. Is that right?

This is correct, yes.

Fabrizio Genovese (Mar 09 2021 at 09:17):

Clearly, since the paper is mainly aimed at engineers (I think there's very little new content for category theorists) we tried to use the simplest language we could think of to express things. As you can indeed see, the paper has no categorical prerequisites and we really start from saying what a category is :smile:

Spencer Breiner (Mar 09 2021 at 16:12):

If you intend this paper to be read by engineers, I strongly encourage you to develop a worked example to carry through the entire paper. Representing, e.g., a test of a system as a set-valued functor is extremely non-intuitive without some concrete details to see how the domain structures align with the math.

Spencer Breiner (Mar 09 2021 at 16:46):

Never mind! I just hadn't reached the example yet. For readability, though, I would suggest moving a naive discussion forward, and using the example to introduce the formal definitions.

John Baez (Mar 09 2021 at 16:51):

Yes, don't count on readers to have much patience...

Fabrizio Genovese (Mar 09 2021 at 17:09):

There's a song in Italian that says something like "If you are good, they throw stones at you; if you are bad, they throw stones at you; whatever you do, wherever you go, you'll always get stones in your face"

Fabrizio Genovese (Mar 09 2021 at 17:10):

So I stopped minding too much about which is the best way of doing things, considering that, as a rule, at least half of the people won't be happy. I can just say that I'm very sorry you ended up in the unhappy bunch this time!

John Baez (Mar 09 2021 at 17:13):

I think it's good to work hard to explain things in a way that people will find easy to understand, and yet expect that some people will complain anyway.

Fabrizio Genovese (Mar 09 2021 at 17:23):

For what I remember, we worked quite hard to make things as understandable as possible :confused: Also, we tried to follow what are considered best practices in engineering papers...

Spencer Breiner (Mar 09 2021 at 17:25):

I haven't understood the details well enough to decide which kind of stones I'm throwing. The main point for me is that mathematicians and engineers prefer to think in diametrically opposed ways. Mathematicians want to "start at the bottom", with minimal assumptions and build up. Engineers want to understand the problem up front, and carve/sand/polish away at it with whatever tools are at hand.

Matteo Capucci (he/him) (Mar 09 2021 at 17:55):

Fabrizio Genovese said:

There's a song in Italian that says something like "If you are good, they throw stones at you; if you are bad, they throw stones at you; whatever you do, wherever you go, you'll always get stones in your face"

What a citation! :laughing:

Matteo Capucci (he/him) (Mar 09 2021 at 17:57):

I don't think people were throwing stones though :) just an opinion about what's the best way to use examples. It doesn't mean that the paper is badly written, imo.

Fabrizio Genovese (Mar 09 2021 at 18:02):

I'm not saying people are throwing stones. I'm saying that every time a choice is made, someone is not happy, it's natural. We wrote that paper following what are the best practices in that field of engineering, that @Giorgos Bakirtzis knows very well. We put in quite a lot of work to make it presentable to that crowd, so it feels a bit strange if someone tells us that it is not the case. :smile:

John Baez (Mar 09 2021 at 18:21):

Spencer wrote:

Mathematicians want to "start at the bottom", with minimal assumptions and build up.

More than engineers, but not all to an equal extent. Category theorists are more obsessed with this than other mathematicians, who usually have some goal in mind that involves lots of assumptions, and get impatient with a gradual build-up.

Spencer Breiner (Mar 09 2021 at 18:27):

There are really two issues here.

One is about the best way to present these ideas to the target audience, and it's true that Giorgos & Cody know that group better than me. All the same, I'm pretty sure your readers eyes will glaze in Section 3, the first technical element of the paper, that is full of definitions. I would push this back to an appendix (or even references), because I don't think they care about logical completeness in the same way that mathematician do. That would leave space for a more detailed discussion of the math as it pertains to the example.

The second issue is actually understanding and testing out the methodology that you've worked out here, which is what I'm really after. I understand most of the pieces, but I'm still having trouble seeing how they fit together. For instance, I'm having trouble imagining a Set-valued functor on the category of $(A\times B,C)$ Mealy machines that would give me some specific insight into the architecture of the machine?

Georgios Bakirtzis (Mar 09 2021 at 18:46):

Hi all, I don't really have time to answer some of these questions my dissertation is due in a couple of weeks and I am focused on that. I promise I will answer @Spencer Breiner questions closer to then. As far as presentation, this is standard practice in the dependability, modeling and security field. I know it was stated before but two of the authors are engineers. Quickly, even in engineering there are fields that are more mathematical than others, e.g., control prefers almost a full mathematical treatment while engineering management and systems modeling requires a plethora of examples from beginning to end. Of course we will find if those choices were good and revise accordingly after the reviews are in. For the second problem I have things to say but will get back to it later. Keep in mind we are working with linear time-invariant systems and moore machines (Mealy machines don't compose nicely as per Spivak)

Georgios Bakirtzis (Mar 09 2021 at 18:47):

Either way I am glad this paper is generating an interesting discussion

Georgios Bakirtzis (May 02 2022 at 15:22):

Our paper is officially accepted to ACM Transactions of Cyber-Physical Systems. The final version after much feedback from @Spencer Breiner and two other anonymous reviewers is here https://arxiv.org/abs/2103.00044 :-)

Jules Hedges (May 02 2022 at 15:57):

Cool! Getting category theory into definitely-not-category-theory journals is always a good thing